diff options
| author | herbelin | 2003-01-19 22:06:34 +0000 |
|---|---|---|
| committer | herbelin | 2003-01-19 22:06:34 +0000 |
| commit | 4dc7a3eb4ac669ead5ee4a1986c4a2310ffda911 (patch) | |
| tree | 0d95d879f4d26f88081241f38f31d64f59a40a56 /toplevel | |
| parent | e70ae0ceeadafc703f01909aeb19273b28e6caef (diff) | |
Restructuration interpréteur de tactique: plus d'évaluation partielle à la définition; suppression TacFunRec, VClosure, VFTactic et VContext; davantage de globalisation statique (notamment pour les tactiques mutuellement récursives); débogueur plus informatif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3532 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 5a4c2fd65e..d0893107a7 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -41,13 +41,13 @@ let constr_to_ast a = let constr_parser_with_glob = Pcoq.map_entry constr_to_ast Constr.constr let globalize_ref vars ref = - match Constrintern.interp_reference vars ref with + match Constrintern.interp_reference (vars,[]) ref with | RRef (loc,a) -> Constrextern.extern_reference loc a | RVar (loc,x) -> Ident (loc,x) | _ -> anomaly "globalize_ref: not a reference" let globalize_ref_term vars ref = - match Constrintern.interp_reference vars ref with + match Constrintern.interp_reference (vars,[]) ref with | RRef (loc,a) -> CRef (Constrextern.extern_reference loc a) | RVar (loc,x) -> CRef (Ident (loc,x)) | c -> Constrextern.extern_rawconstr c @@ -641,7 +641,7 @@ let add_notation_in_scope df c (assoc,n,etyps,onlyparse) sc toks = if onlyparse then None else let r = - interp_rawconstr_gen false Evd.empty (Global.env()) [] false vars c in + interp_rawconstr_gen false Evd.empty (Global.env()) [] false (vars,[]) c in Some (make_old_pp_rule n symbols typs r notation scope vars) in (* Declare the interpretation *) let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 62a08d0492..321ce980b1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -628,7 +628,7 @@ let vernac_back n = Lib.back n (************) (* Commands *) -let vernac_declare_tactic_definition _ l = Tacinterp.add_tacdef l +let vernac_declare_tactic_definition = Tacinterp.add_tacdef let vernac_hints = Auto.add_hints @@ -968,7 +968,7 @@ let vernac_check_guard () = msgnl message let vernac_debug b = - set_debug (if b then Tactic_debug.DebugOn else Tactic_debug.DebugOff) + set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) (**************************) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 8980a7eaa2..30628bfb2b 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -223,7 +223,7 @@ type vernac_expr = (* Commands *) | VernacDeclareTacticDefinition of - loc * (identifier located * raw_tactic_expr) list + rec_flag * (identifier located * raw_tactic_expr) list | VernacHints of string list * hints | VernacHintDestruct of identifier * (bool,unit) location * constr_expr * int * raw_tactic_expr |