diff options
| author | msozeau | 2008-05-11 22:04:26 +0000 |
|---|---|---|
| committer | msozeau | 2008-05-11 22:04:26 +0000 |
| commit | 30443ddaba7a0cc996216b3d692b97e0b05907fe (patch) | |
| tree | 1a1bdadcdf69582262bd6bddc21e9e03215d2871 /contrib | |
| parent | b6c6e36afa8da16a62bf16191baa2531894c54fc (diff) | |
- Cleanup parsing of binders, reducing to a single production for all
binders.
- Change syntax of type class instances to better match the usual syntax of
lemmas/definitions with name first, then arguments ":" instance.
Update theories/Classes accordingly.
- Correct globalization of tactic references when doing Ltac :=/::=, update
documentation.
- Remove the not so useful "(x &)" and "{{x}}" syntaxes from
Program.Utils, and subset_scope as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/xlate.ml | 4 | ||||
| -rw-r--r-- | contrib/subtac/g_subtac.ml4 | 9 |
2 files changed, 7 insertions, 6 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 9f7491d5f4..9db1c7dc42 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1609,8 +1609,8 @@ let rec xlate_vernac = | VernacDeclareTacticDefinition (true, tacs) -> (match List.map (function - ((_, id), _, body) -> - CT_tac_def(CT_ident (string_of_id id), xlate_tactic body)) + (id, _, body) -> + CT_tac_def(reference_to_ct_ID id, xlate_tactic body)) tacs with [] -> assert false | fst::tacs1 -> diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index b7cb7fb233..46bc1a0b86 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -53,7 +53,7 @@ open Constr let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) GEXTEND Gram - GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder_let Constr.binder subtac_nameopt; + GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder subtac_nameopt; subtac_gallina_loc: [ [ g = Vernac.gallina -> loc, g @@ -66,9 +66,9 @@ GEXTEND Gram ; Constr.binder_let: - [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> + [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in - LocalRawAssum ([id], default_binder_kind, typ) + [LocalRawAssum ([id], default_binder_kind, typ)] ] ]; Constr.binder: @@ -141,7 +141,8 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations VERNAC COMMAND EXTEND Subtac_Set_Solver | [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Coqlib.check_required_library ["Coq";"Program";"Tactics"]; - Tacinterp.add_tacdef false [((dummy_loc, id_of_string "obligations_tactic"), true, t)] ] + Tacinterp.add_tacdef false + [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligations_tactic"), true, t)] ] END VERNAC COMMAND EXTEND Subtac_Show_Obligations |