diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-22 10:35:04 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-22 10:35:04 +0000 |
| commit | 6475388a91c899e8bcf7b69b223180025d4f85ff (patch) | |
| tree | 6031dc6e72bb676fa9d9e4f9f2be8ab50c1ca2e3 /parsing/g_proofs.ml4 | |
| parent | 9da09a4da10aa36699538bde01086172c64689eb (diff) | |
reorganisation des niveaux (ex: = est a 70)
Hint Destruct: syntaxe similaire aux autres hints...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_proofs.ml4')
| -rw-r--r-- | parsing/g_proofs.ml4 | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 1cc9f038f..c462c3bdc 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -92,7 +92,7 @@ GEXTEND Gram hyptyp = Constr.constr_pattern; pri = natural; "["; tac = tactic; "]" -> - VernacHintDestruct (local,id,dloc,hyptyp,pri,tac) + VernacHints(local,[],HintsDestruct (id,pri,dloc,hyptyp,tac)) | IDENT "Hint"; local = locality; hintname = base_ident; dbnames = opt_hintbases; ":="; h = hint @@ -115,9 +115,10 @@ GEXTEND Gram [ [ IDENT "Resolve"; c = Constr.constr -> fun name -> HintsResolve [Some name, c] | IDENT "Immediate"; c = Constr.constr -> fun name -> HintsImmediate [Some name, c] | IDENT "Unfold"; qid = global -> fun name -> HintsUnfold [Some name,qid] - | IDENT "Constructors"; c = global -> fun n -> HintsConstructors (n,c) + | IDENT "Constructors"; c = global -> fun n -> + HintsConstructors (Some n,[c]) | IDENT "Extern"; n = natural; c = Constr.constr ; tac = tactic -> - fun name -> HintsExtern (name,n,c,tac) ] ] + fun name -> HintsExtern (Some name,n,c,tac) ] ] ; hints: [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases -> |