From 6475388a91c899e8bcf7b69b223180025d4f85ff Mon Sep 17 00:00:00 2001 From: barras Date: Wed, 22 Oct 2003 10:35:04 +0000 Subject: 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 --- parsing/g_proofs.ml4 | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'parsing/g_proofs.ml4') 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 -> -- cgit v1.2.3