diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-28 08:39:26 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-05-28 08:39:26 +0000 |
commit | 4c0053c66442ec60db46b7b800ff2c1c8bf07a64 (patch) | |
tree | e9713581a40443f5e6dad91ed0eafa53e8a64aad /contrib/correctness | |
parent | 78fe03354fa44a18edbad853ed65a7ba0c3ce6e4 (diff) |
nettoyage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1765 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness')
-rw-r--r-- | contrib/correctness/pcicenv.ml | 2 | ||||
-rw-r--r-- | contrib/correctness/psyntax.ml4 | 8 | ||||
-rw-r--r-- | contrib/correctness/ptactic.ml | 60 |
3 files changed, 24 insertions, 46 deletions
diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml index eecc5eb2f..c1b4b0fa3 100644 --- a/contrib/correctness/pcicenv.ml +++ b/contrib/correctness/pcicenv.ml @@ -42,7 +42,7 @@ let set = mkCast (mkSet, mkType Univ.prop_univ) *) let cci_sign_of ren env = - Penv.fold_all + Penv.fold_all (fun (id,v) sign -> match v with | Penv.TypeV (Ref _ | Array _) -> sign diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index a91bceb8e..e9bb7c88f 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -140,7 +140,11 @@ let ast_zwf_zero loc = (* program -> Coq AST *) -let bdize = Termast.ast_of_constr true (Global.env ()) +let bdize c = + let env = + Global.env_of_context (Pcicenv.cci_sign_of Prename.empty_ren Penv.empty) + in + Termast.ast_of_constr true env c let rec coqast_of_program loc = function | Var id -> let s = string_of_id id in <:ast< ($VAR $s) >> @@ -151,7 +155,7 @@ let rec coqast_of_program loc = function (function Term t -> coqast_of_program t.loc t.desc | _ -> invalid_arg "coqast_of_program") l in - <:ast< (APPLIST $f ($LIST $args)) >> + <:ast< (APPLIST $f ($LIST $args)) >> | Expression c -> bdize c | _ -> invalid_arg "coqast_of_program" diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index 66633277a..6a7a70cf3 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -248,55 +248,29 @@ let register id n = let id' = match n with None -> id | Some id' -> id' in Penv.register id id' -(* -let wrap_save_named b = - let pf_id = Pfedit.get_current_proof_name () in - Command.save_named b; - register pf_id None - -let wrap_save_anonymous b id = - let pf_id = Pfedit.get_current_proof_name () in - Command.save_anonymous b (string_of_id id); - register pf_id (Some id) -*) - let _ = let current_save = Vernacinterp.vinterp_map "SaveNamed" in - add "SaveNamed" - (function [] -> (fun () -> let pf_id = Pfedit.get_current_proof_name () in - current_save [] (); - register pf_id None) - | _ -> assert false) + add "SaveNamed" + (function [] -> (fun () -> let pf_id = Pfedit.get_current_proof_name () in + current_save [] (); + register pf_id None) + | _ -> assert false) let _ = let current_defined = Vernacinterp.vinterp_map "DefinedNamed" in - add "DefinedNamed" - (function [] -> (fun () -> let pf_id = Pfedit.get_current_proof_name () in - current_defined [] (); - register pf_id None) - | _ -> assert false) + add "DefinedNamed" + (function [] -> (fun () -> let pf_id = Pfedit.get_current_proof_name () in + current_defined [] (); + register pf_id None) + | _ -> assert false) let _ = let current_saveanonymous = Vernacinterp.vinterp_map "SaveAnonymous" in - add "SaveAnonymous" - (function [VARG_IDENTIFIER id] -> - (fun () -> let pf_id = Pfedit.get_current_proof_name () in - current_saveanonymous [VARG_IDENTIFIER id] (); - register pf_id (Some id)) - | _ -> assert false) - -(* Old version that does not allow multiple modifications of the "Save" command *) -(* -let _ = - -let _ = add "DefinedNamed" - (function [] -> (fun () -> if_verbose show_script (); - wrap_save_named false) - | _ -> assert false) - -let _ = add "SaveAnonymous" + add "SaveAnonymous" (function [VARG_IDENTIFIER id] -> - (fun () -> if_verbose show_script (); - wrap_save_anonymous true id) - | _ -> assert false) -*) + (fun () -> + let pf_id = Pfedit.get_current_proof_name () in + current_saveanonymous [VARG_IDENTIFIER id] (); + register pf_id (Some id)) + | _ -> assert false) + |