diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-14 09:15:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-14 09:15:38 +0000 |
| commit | 3f1769a8002addec9f53969affd6b4cee1ccbbea (patch) | |
| tree | cab9b33832658113f646ebc38d78cd0bb2c83de3 /toplevel | |
| parent | 8ddd9ba6efcd32a13b4517a4e80c5fc035a951a8 (diff) | |
Ajout option Local à Hint, Hints et HintDestruct
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4163 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 5 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 4 |
2 files changed, 5 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8d21c4d76..1d2ccecbb 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1202,8 +1202,9 @@ let interp c = match c with (* Commands *) | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l - | VernacHints (dbnames,hints) -> vernac_hints dbnames hints - | VernacHintDestruct (id,l,p,n,tac) -> Dhyp.add_destructor_hint id l p n tac + | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints + | VernacHintDestruct (local,id,l,p,n,tac) -> + Dhyp.add_destructor_hint local id l p n tac | VernacSyntacticDefinition (id,c,n) -> vernac_syntactic_definition id c n | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits qid l | VernacReserve (idl,c) -> vernac_reserve idl c diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 22478b880..e03658cfd 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -227,8 +227,8 @@ type vernac_expr = (* Commands *) | VernacDeclareTacticDefinition of rec_flag * (identifier located * raw_tactic_expr) list - | VernacHints of string list * hints - | VernacHintDestruct of + | VernacHints of locality_flag * string list * hints + | VernacHintDestruct of locality_flag * identifier * (bool,unit) location * constr_expr * int * raw_tactic_expr | VernacSyntacticDefinition of identifier * constr_expr * int option | VernacDeclareImplicits of reference * int list option |