diff options
| author | filliatr | 2000-06-21 01:15:42 +0000 |
|---|---|---|
| committer | filliatr | 2000-06-21 01:15:42 +0000 |
| commit | 5378cd45ac34551ea4d265f41b489ff386ea1a49 (patch) | |
| tree | 655fdd402e962863483cdbb40483fcf8b5ab4892 /tactics/equality.ml | |
| parent | 18ca75a6fbaf2a1238a3a2e36f51f1e1bf1c2c68 (diff) | |
portage EAuto et Ring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@513 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 95d61b4cf3..3fac4eb2f5 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -200,12 +200,12 @@ let eq_pattern () = get_pat eq_pattern_mark let not_pattern () = get_pat not_pattern_mark let imp_False_pattern () = get_pat imp_False_pattern_mark -let eq= { eq = put_squel mmk "eq"; - ind = put_squel mmk "eq_ind" ; - rrec = Some (put_squel mmk "eq_rec"); - rect = Some (put_squel mmk "eq_rect"); - congr = put_squel mmk "f_equal" ; - sym = put_squel mmk "sym_eq" } +let eq = { eq = put_squel mmk "eq"; + ind = put_squel mmk "eq_ind" ; + rrec = Some (put_squel mmk "eq_rec"); + rect = Some (put_squel mmk "eq_rect"); + congr = put_squel mmk "f_equal" ; + sym = put_squel mmk "sym_eq" } let build_eq eq = get_squel eq.eq let build_ind eq = get_squel eq.ind @@ -217,12 +217,12 @@ let build_rect eq = let eqT_pattern_mark = put_pat mmk "(eqT ?1 ?2 ?3)" let eqT_pattern () = get_pat eqT_pattern_mark -let eqT= { eq = put_squel mmk "eqT"; - ind = put_squel mmk "eqT_ind" ; - rrec = None; - rect = None; - congr = put_squel mmk "congr_eqT" ; - sym = put_squel mmk "sym_eqT" } +let eqT = { eq = put_squel mmk "eqT"; + ind = put_squel mmk "eqT_ind" ; + rrec = None; + rect = None; + congr = put_squel mmk "congr_eqT" ; + sym = put_squel mmk "sym_eqT" } let idT_pattern_mark = put_pat mmk "(identityT ?1 ?2 ?3)" let idT_pattern () = get_pat idT_pattern_mark |