From f2fc8cbe8b3208626a321398dcb20b5f650b3b91 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 6 Feb 2002 19:37:56 +0000 Subject: gros changement dans mlutil.ml: ajout d'une elimination globale des prop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2456 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/extraction/extraction.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'contrib/extraction/extraction.ml') diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 2ed139b52..7b2e4c9d7 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -205,7 +205,9 @@ let sign_of_arity env c = let vl_of_lbinders = lbinders_fold (fun n _ v a -> - if v = info_arity then (next_ident_away (id_of_name n) (prop_name::a))::a else a) [] + if v = info_arity + then (next_ident_away (id_of_name n) (prop_name::a))::a + else a) [] let vl_of_arity env c = vl_of_lbinders env (List.rev (fst (decompose_prod c))) @@ -542,7 +544,8 @@ and extract_term_info_wt env ctx c t = match kind_of_term c with | Lambda (n, t, d) -> let v = v_of_t env t in - let id = next_ident_away (id_of_name n) [prop_name] in + let id = id_of_name n in + let id = if id=prop_name then anonymous else id in let env' = push_rel_assum (Name id,t) env in let ctx' = (snd v = NotArity) :: ctx in let d' = extract_term_info env' ctx' d in @@ -553,7 +556,8 @@ and extract_term_info_wt env ctx c t = | Info,NotArity -> MLlam (id, d')) | LetIn (n, c1, t1, c2) -> let v = v_of_t env t1 in - let id = next_ident_away (id_of_name n) [prop_name] in + let id = id_of_name n in + let id = if id=prop_name then anonymous else id in let env' = push_rel (Name id,Some c1,t1) env in (match v with | (Info, NotArity) -> -- cgit v1.2.3