Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Revert r15851 "En cours pour bug 2836".

Sorry, was committed mistakenly.

This reverts commit e9cb84af469519b824899c047eed1fed2f8d5af6.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15857 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit e3a62779a8a604d7ee83e72a10254392362d80fe 1 parent 22e70c4
herbelin authored
Showing with 5 additions and 5 deletions.
  1. +5 −5 tactics/equality.ml
View
10 tactics/equality.ml
@@ -232,7 +232,7 @@ let is_applied_rewrite_relation = ref (fun _ _ _ _ -> None)
let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation
(* find_elim determines which elimination principle is necessary to
- eliminate some eq on sort_of_gl. *)
+ eliminate lbeq on sort_of_gl. *)
let find_elim hdcncl lft2rgt dep cls args gl =
let inccl = (cls = None) in
@@ -286,11 +286,11 @@ let type_of_clause gl = function
| None -> pf_concl gl
| Some id -> pf_get_hyp_typ gl id
-let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars frzevars dep_proof_ok gl (hdcncl,args) =
+let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars frzevars dep_proof_ok gl hdcncl =
let isatomic = isProd (whd_zeta hdcncl) in
let dep_fun = if isatomic then dependent else dependent_no_evar in
let dep = dep_proof_ok && dep_fun c (type_of_clause gl cls) in
- let elim = find_elim hdcncl lft2rgt dep cls args gl in
+ let elim = find_elim hdcncl lft2rgt dep cls (snd (decompose_app t)) gl in
general_elim_clause with_evars frzevars tac cls sigma c t l
(match lft2rgt with None -> false | Some b -> b)
{elimindex = None; elimbody = (elim,NoBindings)} gl
@@ -324,7 +324,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
| Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
let lft2rgt = adjust_rewriting_direction args lft2rgt in
leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c (it_mkProd_or_LetIn t rels)
- l with_evars frzevars dep_proof_ok gl (hdcncl,args)
+ l with_evars frzevars dep_proof_ok gl hdcncl
| None ->
try
rewrite_side_tac (!general_rewrite_clause cls
@@ -336,7 +336,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
| Some (hdcncl,args) ->
let lft2rgt = adjust_rewriting_direction args lft2rgt in
leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c
- (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok gl (hdcncl,args)
+ (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok gl hdcncl
| None -> raise e
(* error "The provided term does not end with an equality or a declared rewrite relation." *)

0 comments on commit e3a6277

Please sign in to comment.
Something went wrong with that request. Please try again.