diff options
| author | herbelin | 2003-11-09 15:12:54 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-09 15:12:54 +0000 |
| commit | fc403f2f912cfceef5ff96af379b6e9d912f0c03 (patch) | |
| tree | c45401f25a7211f5a761d5767f908936830bd7c1 | |
| parent | 5db7bbe35613004fc2cdac3096b3a1b26aa276bc (diff) | |
Traduction semantique des InHyp de clause en InHypValue si local def; simplification suite fusion eq/eqT
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4840 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/equality.ml | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index b537d5e689..2649d21d4e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -189,11 +189,8 @@ let necessary_elimination sort_arity sort = (str "no primitive equality on proofs") let find_eq_pattern aritysort sort = - match necessary_elimination aritysort sort with - | Set_Type -> (build_coq_eq_data ()).eq - | Type_Type -> (build_coq_idT_data ()).eq - | Set_SetorProp -> (build_coq_eq_data ()).eq - | Type_SetorProp -> (build_coq_eq_data ()).eq + (* "eq" now accept arguments in Type and elimination to Type *) + Coqlib.build_coq_eq () (* [find_positions t1 t2] @@ -1157,9 +1154,7 @@ let unfold_body x gl = (pr_id x ++ str" is not a defined hypothesis") in let aft = afterHyp x gl in let hl = List.fold_right - (fun (y,yval,_) cl -> - if yval=None then InHypType y :: cl - else InHyp y :: InHypType y :: cl) aft [] in + (fun (y,yval,_) cl -> (y,(InHyp,ref None)) :: cl) aft [] in let xvar = mkVar x in let rfun _ _ c = replace_term xvar xval c in tclTHENLIST |