diff options
| author | letouzey | 2012-10-16 16:24:23 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-16 16:24:23 +0000 |
| commit | 15daaa856a6dd1f97845c4f24fe27eaf4cdbdda0 (patch) | |
| tree | 0b5a33550e30f286ef65e7c12ea452c2b86da409 /grammar | |
| parent | 3b5927180128a4e8f10f7437641ff3af220194b3 (diff) | |
Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15896 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 14 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 6 |
2 files changed, 11 insertions, 9 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index a3c94c5d4f..9c31e2c829 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -190,7 +190,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = | None -> <:expr< fun e x -> out_gen $make_globwit loc rawtyp$ - (Tacinterp.intern_genarg e + (Tacintern.intern_genarg e (Genarg.in_gen $make_rawwit loc rawtyp$ x)) >> | Some f -> <:expr< $lid:f$>> in let interp = match f with @@ -206,7 +206,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = | None -> <:expr< fun s x -> out_gen $make_globwit loc globtyp$ - (Tacinterp.subst_genarg s + (Tacsubst.subst_genarg s (Genarg.in_gen $make_globwit loc globtyp$ x)) >> | Some f -> <:expr< $lid:f$>> in let se = mlexpr_of_string s in @@ -222,14 +222,16 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = <:str_item< value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; <:str_item< do { + Tacintern.add_intern_genarg $se$ + (fun e x -> + (Genarg.in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x)))); Tacinterp.add_interp_genarg $se$ - ((fun e x -> - (Genarg.in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x)))), (fun ist gl x -> let (sigma,a_interp) = $interp$ ist gl (out_gen $globwit$ x) in - (sigma , Genarg.in_gen $wit$ a_interp)), + (sigma , Genarg.in_gen $wit$ a_interp)); + Tacsubst.add_genarg_subst $se$ (fun subst x -> - (Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x))))); + (Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x)))); Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a)) (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 09c49b3b61..cebfaa6150 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -128,7 +128,7 @@ let rec possibly_empty_subentries loc = function <:expr< match Genarg.default_empty_value $rawwit$ with [ None -> failwith "" | Some v -> - Tacinterp.intern_genarg Tacinterp.fully_empty_glob_sign + Tacintern.intern_genarg Tacintern.fully_empty_glob_sign (Genarg.in_gen $rawwit$ v) ] >> | GramTerminal _ | GramNonTerminal(_,_,_,_) -> (* This does not parse epsilon (this Exit is static time) *) @@ -159,11 +159,11 @@ let declare_tactic loc s cl = declare_str_items loc [ <:str_item< do { try - let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in + let _=Tacintern.add_tactic $se$ $make_fun_clauses loc s cl$ in List.iter (fun (s,l) -> match l with [ Some l -> - Tacinterp.add_primitive_tactic s + Tacintern.add_primitive_tactic s (Tacexpr.TacAtom($default_loc$, Tacexpr.TacExtend($default_loc$,$se$,l))) | None -> () ]) |