diff options
| -rw-r--r-- | pretyping/evarutil.ml | 4 | ||||
| -rw-r--r-- | theories/Logic/Eqdep_dec.v | 16 |
2 files changed, 10 insertions, 10 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 87fd80963..77366d601 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -304,8 +304,8 @@ let rec solve_simple_eqn conv_algo isevars ((pbty,t1,t2) as pb) = | (true,true) -> if num_of_evar t1 = num_of_evar t2 then solve_refl conv_algo isevars t1 t2 - else if Array.length(args_of_const t1) < - Array.length(args_of_const t2) then + else if Array.length(snd (destEvar t1)) < + Array.length(snd (destEvar t2)) then Some (evar_define isevars t2 t1) else Some (evar_define isevars t1 t2) diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index ecf73f99c..29a8b0a66 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -43,8 +43,8 @@ Section DecidableEqDep. Variable A: Type. - Local comp: (x,y,y':A)x==y->x==y'->y==y' := - [x,y,y',eq1,eq2](eqT_ind ? ? [a]a==y' eq2 ? eq1). + Local comp [x,y,y':A]: x==y->x==y'->y==y' := + [eq1,eq2](eqT_ind ? ? [a]a==y' eq2 ? eq1). Remark trans_sym_eqT: (x,y:A)(u:x==y)(comp u u)==(refl_eqT ? y). Intros. @@ -59,11 +59,11 @@ Save. Variable x: A. - Local nu: (y:A)x==y->x==y := - [y,u]Case (eq_dec x y) of - [H:x==y]H - [H:~x==y](False_ind ? (H u)) - end. + Local nu [y:A]: x==y->x==y := + [u]Cases (eq_dec x y) of + (or_introl eqxy) => eqxy + | (or_intror neqxy) => (False_ind ? (neqxy u)) + end. Remark nu_constant : (y:A)(u,v:x==y) (nu u)==(nu v). Intros. @@ -75,7 +75,7 @@ Case y0; Trivial. Save. - Local nu_inv: (y:A)x==y->x==y := [y,v](comp (nu (refl_eqT ? x)) v). + Local nu_inv [y:A]: x==y->x==y := [v](comp (nu (refl_eqT ? x)) v). Remark nu_left_inv : (y:A)(u:x==y) (nu_inv (nu u))==u. |