From d0434af99ebb2b7550b8d67ee7925f99043ae7f2 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 25 Dec 2000 21:15:08 +0000 Subject: Bug confusion existS/sigS git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1210 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/equality.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index 2108301c3..aa031ade6 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -189,7 +189,7 @@ type sigma_type = { proj2 : constr; elim : constr; intro : constr; - ex : constr } + typ : constr } let mmk = make_module_marker [ "Prelude"; "Logic_Type"; "Specif"; "Logic" ] @@ -678,14 +678,14 @@ let build_sigma_set () = proj2 = constant ["Specif"] "projS2"; elim = constant ["Specif"] "sigS_rec"; intro = constant ["Specif"] "existS"; - ex = constant ["Specif"] "sigS" } + typ = constant ["Specif"] "sigS" } let build_sigma_type () = { proj1 = constant ["Specif"] "projT1"; proj2 = constant ["Specif"] "projT2"; elim = constant ["Specif"] "sigT_rec"; intro = constant ["Specif"] "existT"; - ex = constant ["Specif"] "sigT" } + typ = constant ["Specif"] "sigT" } (* returns the sigma type (sigS, sigT) with the respective constructor depending on the sort *) @@ -711,7 +711,7 @@ let find_sigma_data s = let make_tuple env sigma (prev_lind,rterm,rty) lind = assert (dependent (mkRel lind) rty); - let {intro = exist_term; ex = sig_term} = + let {intro = exist_term; typ = sig_term} = find_sigma_data (get_sort_of env sigma rty) in let a = type_of env sigma (mkRel lind) in let na = fst (lookup_rel_type lind env) in @@ -760,7 +760,7 @@ let minimal_free_rels env sigma (c,cty) = *) let sig_clausale_forme env sigma sort_of_ty siglen ty (dFLT,dFLTty) = - let { ex = exist_term } = find_sigma_data sort_of_ty in + let { intro = exist_term } = find_sigma_data sort_of_ty in let rec sigrec_clausale_forme siglen ty = if siglen = 0 then (* We obtain the components dependent in dFLT by matching *) -- cgit v1.2.3