diff options
| author | barras | 2006-10-27 21:21:17 +0000 |
|---|---|---|
| committer | barras | 2006-10-27 21:21:17 +0000 |
| commit | 5b8e645b675b6b2efac8e13c29da5e984248e507 (patch) | |
| tree | f39598f12eefa82801eb3adb9b954edf4b56cadc /tactics | |
| parent | c5e8c731ede28ba4f734bbd143c7d7e5a05c365a (diff) | |
simplif de la partie ML de ring/field
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9302 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f7e4a97506..ee70c326f1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1824,6 +1824,8 @@ and interp_genarg ist gl x = | BindingsArgType -> in_gen wit_bindings (interp_bindings ist gl (out_gen globwit_bindings x)) + | List0ArgType ConstrArgType -> interp_genarg_constr_list0 ist gl x + | List1ArgType ConstrArgType -> interp_genarg_constr_list1 ist gl x | List0ArgType _ -> app_list0 (interp_genarg ist gl) x | List1ArgType _ -> app_list1 (interp_genarg ist gl) x | OptArgType _ -> app_opt (interp_genarg ist gl) x @@ -1836,6 +1838,16 @@ and interp_genarg ist gl x = | None -> lookup_interp_genarg s ist gl x +and interp_genarg_constr_list0 ist gl x = + let lc = out_gen (wit_list0 globwit_constr) x in + let lc = pf_interp_constr_list ist gl lc in + in_gen (wit_list0 wit_constr) lc + +and interp_genarg_constr_list1 ist gl x = + let lc = out_gen (wit_list1 globwit_constr) x in + let lc = pf_interp_constr_list ist gl lc in + in_gen (wit_list1 wit_constr) lc + (* Interprets the Match expressions *) and interp_match ist g lz constr lmr = let rec apply_match_subterm ist nocc (id,c) csr mt = |