diff options
| author | msozeau | 2006-04-07 15:08:12 +0000 |
|---|---|---|
| committer | msozeau | 2006-04-07 15:08:12 +0000 |
| commit | 26ca22424b286f5ff22a1fa97c38d15e224b3dc2 (patch) | |
| tree | 190e12acf505e47d3a81ef0fd625a405ff782c04 /contrib/subtac/subtac_command.mli | |
| parent | 5f9b04da0f3c72f4b582cd094edae721b1bc9a9e (diff) | |
- Documentation of the Program tactics.
- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists.
Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop.
- Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/subtac_command.mli')
| -rw-r--r-- | contrib/subtac/subtac_command.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli index 6c1b0103ff..e1bbbbb5b0 100644 --- a/contrib/subtac/subtac_command.mli +++ b/contrib/subtac/subtac_command.mli @@ -16,26 +16,26 @@ val interp_gen : ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign -> - constr_expr -> evar_map * constr + constr_expr -> constr val interp_constr : evar_defs ref -> - env -> constr_expr -> evar_map * constr + env -> constr_expr -> constr val interp_type : evar_defs ref -> env -> ?impls:full_implicits_env -> - constr_expr -> evar_map * constr + constr_expr -> constr val interp_casted_constr : evar_defs ref -> env -> ?impls:full_implicits_env -> - constr_expr -> types -> evar_map * constr + constr_expr -> types -> constr val interp_open_constr : evar_defs ref -> env -> constr_expr -> constr val interp_constr_judgment : evar_defs ref -> env -> - constr_expr -> evar_defs * unsafe_judgment + constr_expr -> unsafe_judgment val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list val recursive_message : global_reference array -> std_ppcmds val build_recursive : |