diff options
| author | filliatr | 2001-03-30 15:06:48 +0000 |
|---|---|---|
| committer | filliatr | 2001-03-30 15:06:48 +0000 |
| commit | f5f283ec29d79a64d8fdda92823fe606a475e625 (patch) | |
| tree | 9ce71088b933336bad04250d32e9271498576eb0 /parsing | |
| parent | d7550d7625f9eb9bc9c0e88dabd744f6b1530891 (diff) | |
branchement extraction (bytecode seulement)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1509 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/coqlib.ml | 7 | ||||
| -rw-r--r-- | parsing/coqlib.mli | 2 | ||||
| -rw-r--r-- | parsing/g_zsyntax.mli | 2 |
3 files changed, 11 insertions, 0 deletions
diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml index 0aae508e52..3250c8db79 100644 --- a/parsing/coqlib.ml +++ b/parsing/coqlib.ml @@ -206,6 +206,12 @@ let coq_existT_ref = lazy (reference "Logic_Type" "existT") let coq_not_ref = lazy (reference "Logic" "not") let coq_False_ref = lazy (reference "Logic" "False") let coq_sumbool_ref = lazy (reference "Specif" "sumbool") +let coq_sig_ref = lazy (reference "Specif" "sig") + +(* Pattern "(sig ?1 ?2)" *) +let coq_sig_pattern = + lazy (PApp (PRef (Lazy.force coq_sig_ref), + [| PMeta (Some 1); PMeta (Some 2) |])) (* Patterns "(eq ?1 ?2 ?3)", "(eqT ?1 ?2 ?3)" and "(idT ?1 ?2 ?3)" *) let coq_eq_pattern_gen eq = @@ -274,3 +280,4 @@ let build_coq_eqdec_pattern () = Lazy.force coq_eqdec_pattern let build_coq_arrow_pattern () = Lazy.force coq_arrow_pattern let build_coq_refl_rel1_pattern () = Lazy.force coq_refl_rel1_pattern let build_coq_refl_rel2_pattern () = Lazy.force coq_refl_rel2_pattern +let build_coq_sig_pattern () = Lazy.force coq_sig_pattern diff --git a/parsing/coqlib.mli b/parsing/coqlib.mli index 13699a2428..99481982da 100644 --- a/parsing/coqlib.mli +++ b/parsing/coqlib.mli @@ -118,3 +118,5 @@ val build_coq_refl_rel2_pattern : constr_pattern delayed (* ["(?1 -> ?2)"] *) val build_coq_arrow_pattern : constr_pattern delayed +(* ["(sig ?1 ?2)"] *) +val build_coq_sig_pattern : constr_pattern delayed diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli index a8370f6306..afda96bd96 100644 --- a/parsing/g_zsyntax.mli +++ b/parsing/g_zsyntax.mli @@ -9,3 +9,5 @@ (*i $Id$ i*) (* Nice syntax for integers. *) + +val z_of_string : bool -> string -> Coqast.loc -> Coqast.t |