diff options
| author | herbelin | 2003-03-29 16:47:26 +0000 |
|---|---|---|
| committer | herbelin | 2003-03-29 16:47:26 +0000 |
| commit | 7bdfef00a00a6c7403166bcaadc9cdfcd0e92451 (patch) | |
| tree | c8e57c7de1998e89ed48289f8fb015fd7fa022f9 /tactics | |
| parent | b2f779cf923cab0d5c8990678fd9568250e014c8 (diff) | |
eq fusionne avec eqT et devient par défaut sur Type,
idem pour ex et exT, ex2 et exT2, all et allT
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/setoid_replace.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 3eee019bac..27fffec56f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -134,7 +134,7 @@ let abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl = let (e,sym) = match kind_of_term (hnf_type_of gl t1) with | Sort (Prop(Pos)) -> (eq,sym_eq) - | Sort (Type(_)) -> (eqt,sym_eqt) + | Sort (Type(_)) -> (eq,sym_eq) | _ -> error "replace" in (tclTHENLAST (elim_type (applist (e, [t1;c1;c2]))) @@ -209,7 +209,7 @@ let find_eq_pattern aritysort sort = | 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_eqT_data.eq () + | Type_SetorProp -> build_coq_eq_data.eq () (* [find_positions t1 t2] diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 389943f30b..4468fd4d35 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -83,7 +83,7 @@ let coq_fleche = lazy(constant ["Setoid"] "fleche") (* Coq constants *) -let coqeq = lazy(global_constant ["Logic_Type"] "eqT") +let coqeq = lazy(global_constant ["Logic"] "eq") let coqconj = lazy(global_constant ["Logic"] "conj") let coqand = lazy(global_constant ["Logic"] "and") |