diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
| commit | e4282ea99c664d8d58067bee199cbbcf881b60d5 (patch) | |
| tree | d4c4a873eb055c728666f367469fa26c3417793a /contrib/subtac/subtac_pretyping.ml | |
| parent | a0a94c1340a63cdb824507b973393882666ba52a (diff) | |
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'contrib/subtac/subtac_pretyping.ml')
| -rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 07a75720..3ae7c95d 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping.ml 11574 2008-11-10 13:45:05Z msozeau $ *) +(* $Id: subtac_pretyping.ml 12187 2009-06-13 19:36:59Z msozeau $ *) open Global open Pp @@ -84,13 +84,6 @@ let find_with_index x l = | [] -> raise Not_found in aux 0 l -let list_split_at index l = - let rec aux i acc = function - hd :: tl when i = index -> (List.rev acc), tl - | hd :: tl -> aux (succ i) (hd :: acc) tl - | [] -> failwith "list_split_at: Invalid argument" - in aux 0 [] l - open Vernacexpr let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env @@ -136,9 +129,9 @@ let subtac_process env isevars id bl c tycon = open Subtac_obligations -let subtac_proof kind env isevars id bl c tycon = +let subtac_proof kind hook env isevars id bl c tycon = let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in let evm' = Subtac_utils.evars_of_term evm evm' coqt in let evars, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in - add_definition id def ty ~implicits:imps ~kind:kind evars + add_definition id def ty ~implicits:imps ~kind ~hook evars |