diff options
| author |  puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:28:09 +0000 |
|---|---|---|
| committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:28:09 +0000 |
| commit | 07c2866314a27a9f5cbf42edab8c172d9f62c8de (patch) | |
| tree | ee19c5bedc2f9ccde6340890dd69d30bc2a84546 /pretyping/evarutil.ml | |
| parent | ffb0c213b5341927a6b1cea245432d14695d5c33 (diff) | |
Evarutil: replaced some generic = on constr by destructors
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14352 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 2e940583c..a13c24908 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -420,7 +420,7 @@ let shrink_context env subst ty = (* We merge the contexts (optimization) *) let rec shrink_rel i subst rel_subst rev_rel_sign = match subst,rev_rel_sign with - | (id,c)::subst,_::rev_rel_sign when c = mkRel i -> + | (id,c)::subst,_::rev_rel_sign when isRel c && destRel c = i -> shrink_rel (i-1) subst (mkVar id::rel_subst) rev_rel_sign | _ -> substl_rel_context rel_subst (List.rev rev_rel_sign), @@ -428,7 +428,7 @@ let shrink_context env subst ty = in let rec shrink_named subst named_subst rev_named_sign = match subst,rev_named_sign with - | (id,c)::subst,(id',b',t')::rev_named_sign when c = mkVar id' -> + | (id,c)::subst,(id',b',t')::rev_named_sign when isVar c && destVar c = id' -> shrink_named subst ((id',mkVar id)::named_subst) rev_named_sign | _::_, [] -> let nrel = List.length rel_sign in @@ -928,7 +928,7 @@ let are_canonical_instances args1 args2 env = let n2 = Array.length args2 in let rec aux n = function | (id,_,c)::sign - when n < n1 && args1.(n) = mkVar id && args1.(n) = args2.(n) -> + when n < n1 && isVar args1.(n) && destVar args1.(n) = id && eq_constr args1.(n) args2.(n) -> aux (n+1) sign | [] -> let rec aux2 n = |