summaryrefslogtreecommitdiff
path: root/contrib/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac')
-rw-r--r--contrib/subtac/g_subtac.ml46
-rw-r--r--contrib/subtac/subtac.ml5
-rw-r--r--contrib/subtac/subtac_cases.ml8
-rw-r--r--contrib/subtac/subtac_classes.ml43
-rw-r--r--contrib/subtac/subtac_classes.mli10
-rw-r--r--contrib/subtac/subtac_coercion.ml65
-rw-r--r--contrib/subtac/subtac_command.ml27
-rw-r--r--contrib/subtac/subtac_command.mli1
-rw-r--r--contrib/subtac/subtac_obligations.ml3
-rw-r--r--contrib/subtac/subtac_pretyping.ml11
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml51
-rw-r--r--contrib/subtac/test/ListsTest.v20
-rw-r--r--contrib/subtac/test/take.v18
13 files changed, 132 insertions, 136 deletions
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 88243b60..4cf5336d 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -14,7 +14,7 @@
Syntax for the subtac terms and types.
Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
-(* $Id: g_subtac.ml4 10919 2008-05-11 22:04:26Z msozeau $ *)
+(* $Id: g_subtac.ml4 11282 2008-07-28 11:51:53Z msozeau $ *)
open Flags
@@ -139,10 +139,10 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations
END
VERNAC COMMAND EXTEND Subtac_Set_Solver
-| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [
+| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
Coqlib.check_required_library ["Coq";"Program";"Tactics"];
Tacinterp.add_tacdef false
- [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligations_tactic"), true, t)] ]
+ [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligation_tactic"), true, t)] ]
END
VERNAC COMMAND EXTEND Subtac_Show_Obligations
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index a59ad6f5..7bfa107b 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac.ml 11150 2008-06-19 11:38:27Z msozeau $ *)
+(* $Id: subtac.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Global
open Pp
@@ -229,7 +229,8 @@ let subtac (loc, command) =
debug 2 (Himsg.explain_pretype_error env exn);
raise e
- | (Stdpp.Exc_located (loc, e')) as e ->
+ | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
+ Stdpp.Exc_located (loc, e') as e) ->
debug 2 (str "Parsing exception: ");
(match e' with
| Type_errors.TypeError (env, exn) ->
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index c7182bd2..04bf54d3 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_cases.ml 11154 2008-06-19 18:42:19Z msozeau $ *)
+(* $Id: subtac_cases.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
open Cases
open Util
@@ -2056,8 +2056,10 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars)
tomatchs sign (lift tomatchs_len t)
in
- let arity =
- it_mkProd_or_LetIn (lift neqs arity) (context_of_arsign eqs)
+ let neqs, arity =
+ let ctx = context_of_arsign eqs in
+ let neqs = List.length ctx in
+ neqs, it_mkProd_or_LetIn (lift neqs arity) ctx
in
let lets, matx =
(* Type the rhs under the assumption of equations *)
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 15addb44..9a5539e2 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtac_classes.ml 11047 2008-06-03 23:08:00Z msozeau $ i*)
+(*i $Id: subtac_classes.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
open Pretyping
open Evd
@@ -73,26 +73,18 @@ let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
let type_ctx_instance isevars env ctx inst subst =
List.fold_left2
(fun (subst, instctx) (na, _, t) ce ->
- let t' = replace_vars subst t in
+ let t' = substl subst t in
let c = interp_casted_constr_evars isevars env ce t' in
+ isevars := resolve_typeclasses ~onlyargs:true ~fail:true env !isevars;
let d = na, Some c, t' in
- (na, c) :: subst, d :: instctx)
+ c :: subst, d :: instctx)
(subst, []) (List.rev ctx) inst
-(*let superclass_ce = CRef (Ident (dummy_loc, id_of_string ".superclass"))*)
-
let type_class_instance_params isevars env id n ctx inst subst =
List.fold_left2
(fun (subst, instctx) (na, _, t) ce ->
let t' = replace_vars subst t in
- let c =
-(* if ce = superclass_ce then *)
- (* (\* Control over the evars which are direct superclasses to avoid partial instanciations *)
- (* in instance search. *\) *)
- (* Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' *)
- (* else *)
- interp_casted_constr_evars isevars env ce t'
- in
+ let c = interp_casted_constr_evars isevars env ce t' in
let d = na, Some c, t' in
(na, c) :: subst, d :: instctx)
(subst, []) (List.rev ctx) inst
@@ -140,9 +132,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
let k, ctx', imps, subst =
let c = Command.generalize_constr_expr tclass ctx in
let c', imps = interp_type_evars_impls ~evdref:isevars env c in
- let ctx, c = Classes.decompose_named_assum c' in
+ let ctx, c = Sign.decompose_prod_assum c' in
let cl, args = Typeclasses.dest_class_app c in
- cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
+ cl, ctx, imps, (List.rev (Array.to_list args))
in
let id =
match snd instid with
@@ -155,11 +147,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
Termops.next_global_ident_away false i (Termops.ids_of_context env)
in
- let env' = Classes.push_named_context ctx' env in
+ let env' = push_rel_context ctx' env in
isevars := Evarutil.nf_evar_defs !isevars;
isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars;
let sigma = Evd.evars_of !isevars in
- let substctx = Typeclasses.nf_substitution sigma subst in
+ let substctx = List.map (Evarutil.nf_evar sigma) subst in
let subst, _propsctx =
let props =
List.map (fun (x, l, d) ->
@@ -172,8 +164,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
List.fold_left
(fun (props, rest) (id,_,_) ->
try
- let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in
- let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+ let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
+ let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
c :: props, rest'
with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
@@ -184,20 +176,13 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
else
type_ctx_instance isevars env' k.cl_props props substctx
in
- let inst_constr, ty_constr = instance_constructor k (List.rev_map snd subst) in
+ let inst_constr, ty_constr = instance_constructor k (List.rev subst) in
isevars := Evarutil.nf_evar_defs !isevars;
- let term = Evarutil.nf_isevar !isevars (it_mkNamedLambda_or_LetIn inst_constr ctx')
- and termtype = Evarutil.nf_isevar !isevars (it_mkNamedProd_or_LetIn ty_constr ctx')
+ let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx')
+ and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx')
in
isevars := undefined_evars !isevars;
Evarutil.check_evars env Evd.empty !isevars termtype;
-(* let imps = *)
-(* Util.list_map_i *)
-(* (fun i binder -> *)
-(* match binder with *)
-(* ExplByPos (i, Some na), (true, true)) *)
-(* 1 ctx *)
-(* in *)
let hook gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
let inst = Typeclasses.new_instance k pri global cst in
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index 43f00107..afb0d38d 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtac_classes.mli 10797 2008-04-15 13:19:33Z msozeau $ i*)
+(*i $Id: subtac_classes.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
(*i*)
open Names
@@ -26,11 +26,11 @@ open Classes
val type_ctx_instance : Evd.evar_defs ref ->
Environ.env ->
- (Names.identifier * 'a * Term.constr) list ->
+ ('a * Term.constr option * Term.constr) list ->
Topconstr.constr_expr list ->
- (Names.identifier * Term.constr) list ->
- (Names.identifier * Term.constr) list *
- (Names.identifier * Term.constr option * Term.constr) list
+ Term.constr list ->
+ Term.constr list *
+ ('a * Term.constr option * Term.constr) list
val new_instance :
?global:bool ->
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index b45e23d0..b046f0b3 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -6,7 +6,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_coercion.ml 11143 2008-06-18 15:52:42Z msozeau $ *)
+(* $Id: subtac_coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
open Util
open Names
@@ -111,41 +111,31 @@ module Coercion = struct
: (Term.constr -> Term.constr) option
=
let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
-(* (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++ *)
-(* str " and "++ my_print_constr env y ++ *)
-(* str " with evars: " ++ spc () ++ *)
-(* my_print_evardefs !isevars); *)
-(* with _ -> ()); *)
let rec coerce_unify env x y =
-(* (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++ *)
-(* str " to "++ my_print_constr env y) *)
-(* with _ -> ()); *)
let x = hnf env isevars x and y = hnf env isevars y in
try
isevars := the_conv_x_leq env x y !isevars;
- (* (try debug 1 (str "Unified " ++ (my_print_constr env x) ++ *)
- (* str " and "++ my_print_constr env y); *)
- (* with _ -> ()); *)
None
with Reduction.NotConvertible -> coerce' env x y
and coerce' env x y : (Term.constr -> Term.constr) option =
let subco () = subset_coerce env isevars x y in
+ let dest_prod c =
+ match Reductionops.decomp_n_prod env (evars_of !isevars) 1 c with
+ | [(na,b,t)], c -> (na,t), c
+ | _ -> raise NoSubtacCoercion
+ in
let rec coerce_application typ typ' c c' l l' =
let len = Array.length l in
let rec aux tele typ typ' i co =
-(* (try trace (str "coerce_application.aux from " ++ (my_print_constr env x) ++ *)
-(* str " to "++ my_print_constr env y *)
-(* ++ str "in env:" ++ my_print_env env); *)
-(* with _ -> ()); *)
if i < len then
let hdx = l.(i) and hdy = l'.(i) in
try isevars := the_conv_x_leq env hdx hdy !isevars;
- let (n, eqT, restT) = destProd typ in
- let (n', eqT', restT') = destProd typ' in
+ let (n, eqT), restT = dest_prod typ in
+ let (n', eqT'), restT' = dest_prod typ' in
aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
with Reduction.NotConvertible ->
- let (n, eqT, restT) = destProd typ in
- let (n', eqT', restT') = destProd typ' in
+ let (n, eqT), restT = dest_prod typ in
+ let (n', eqT'), restT' = dest_prod typ' in
let _ =
try isevars := the_conv_x_leq env eqT eqT' !isevars
with Reduction.NotConvertible -> raise NoSubtacCoercion
@@ -163,12 +153,12 @@ module Coercion = struct
[| eqT; hdx; pred; x; hdy; evar|]) in
aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x))
else Some co
- in aux [] typ typ' 0 (fun x -> x)
+ in
+ if isEvar c || isEvar c' then
+ (* Second-order unification needed. *)
+ raise NoSubtacCoercion;
+ aux [] typ typ' 0 (fun x -> x)
in
-(* (try trace (str "coerce' from " ++ (my_print_constr env x) ++ *)
-(* str " to "++ my_print_constr env y *)
-(* ++ str "in env:" ++ my_print_env env); *)
-(* with _ -> ()); *)
match (kind_of_term x, kind_of_term y) with
| Sort s, Sort s' ->
(match s, s' with
@@ -179,13 +169,6 @@ module Coercion = struct
| Prod (name, a, b), Prod (name', a', b') ->
let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in
let env' = push_rel (name', None, a') env in
-
-(* let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in *)
-(* let name'' = Name (Nameops.next_ident_away (id_of_string "x'") (Termops.ids_of_context env)) in *)
-(* let env'' = push_rel (name'', Some (app_opt c1 (mkRel 1)), lift 1 a) env' in *)
-(* let c2 = coerce_unify env'' (liftn 1 1 b) (lift 1 b') in *)
-(* mkLetIn (name'', app_opt c1 (mkRel 1), (lift 1 a), *)
-
let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
(* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
let coec1 = app_opt c1 (mkRel 1) in
@@ -295,7 +278,6 @@ module Coercion = struct
and subset_coerce env isevars x y =
match disc_subset x with
Some (u, p) ->
- (* trace (str "Inserting projection "); *)
let c = coerce_unify env u y in
let f x =
app_opt c (mkApp ((Lazy.force sig_).proj1,
@@ -423,7 +405,11 @@ module Coercion = struct
isevars, { uj_val = app_opt ct j.uj_val;
uj_type = typ' }
-
+ let inh_coerce_to_prod loc env isevars t =
+ let typ = whd_betadeltaiota env (evars_of isevars) (snd t) in
+ let _, typ' = mu env isevars typ in
+ isevars, (fst t, typ')
+
let inh_coerce_to_fail env evd rigidonly v t c1 =
if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
then
@@ -504,14 +490,13 @@ module Coercion = struct
None -> 0, 0
| Some (init, cur) -> init, cur
in
- (* a little more effort to get products is needed *)
- try let rels, rng = decompose_prod_n nabs t in
+ try
+ let rels, rng = Reductionops.decomp_n_prod env (evars_of isevars) nabs t in
(* The final range free variables must have been replaced by evars, we accept only that evars
in rng are applied to free vars. *)
- if noccur_with_meta 0 (succ nabsinit) rng then (
-(* trace (str "No occur between 0 and " ++ int (succ nabsinit)); *)
+ if noccur_with_meta 1 (succ nabs) rng then (
let env', t, t' =
- let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
+ let env' = push_rel_context rels env in
env', rng, lift nabs t'
in
try
@@ -523,6 +508,4 @@ module Coercion = struct
error_cannot_coerce env' sigma (t, t'))
else isevars
with _ -> isevars
-(* trace (str "decompose_prod_n failed"); *)
-(* raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *)
end
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 5bff6ad1..a2f54b02 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -350,9 +350,27 @@ let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
let push_named_context = List.fold_right push_named
+let check_evars env initial_sigma evd c =
+ let sigma = evars_of evd in
+ let c = nf_evar sigma c in
+ let rec proc_rec c =
+ match kind_of_term c with
+ | Evar (evk,args) ->
+ assert (Evd.mem sigma evk);
+ if not (Evd.mem initial_sigma evk) then
+ let (loc,k) = evar_source evk evd in
+ (match k with
+ | QuestionMark _ -> ()
+ | _ ->
+ let evi = nf_evar_info sigma (Evd.find sigma evk) in
+ Pretype_errors.error_unsolvable_implicit loc env sigma evi k None)
+ | _ -> iter_constr proc_rec c
+ in proc_rec c
+
let interp_recursive fixkind l boxed =
let env = Global.env() in
let fixl, ntnl = List.split l in
+ let kind = if fixkind <> Command.IsCoFixpoint then Fixpoint else CoFixpoint in
let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in
(* Interp arities allowing for unresolved types *)
@@ -384,20 +402,17 @@ let interp_recursive fixkind l boxed =
let rec_sign = nf_named_context_evar (evars_of evd) rec_sign in
let recdefs = List.length rec_sign in
-(* List.iter (check_evars env_rec Evd.empty evd) fixdefs; *)
-(* List.iter (check_evars env Evd.empty evd) fixtypes; *)
-(* check_mutuality env kind (List.combine fixnames fixdefs); *)
+ List.iter (check_evars env_rec Evd.empty evd) fixdefs;
+ List.iter (check_evars env Evd.empty evd) fixtypes;
+ Command.check_mutuality env kind (List.combine fixnames fixdefs);
(* Russell-specific code *)
(* Get the interesting evars, those that were not instanciated *)
let isevars = Evd.undefined_evars evd in
- trace (str "got undefined evars" ++ Evd.pr_evar_defs isevars);
let evm = Evd.evars_of isevars in
- trace (str "got the evm, recdefs is " ++ int recdefs);
(* Solve remaining evars *)
let rec collect_evars id def typ imps =
- let _ = try trace (str "In collect evars, isevars is: " ++ Evd.pr_evar_defs isevars) with _ -> () in
(* Generalize by the recursive prototypes *)
let def =
Termops.it_mkNamedLambda_or_LetIn def rec_sign
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index 27520867..3a6a351b 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -42,6 +42,7 @@ val interp_binder : Evd.evar_defs ref ->
Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr
+
val build_recursive :
(fixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 55cdc7c4..a393e2c9 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -119,7 +119,7 @@ let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
let freeze () = !from_prg, !default_tactic_expr
let unfreeze (v, t) = from_prg := v; set_default_tactic t
let init () =
- from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligations_tactic" [])
+ from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligation_tactic" [])
let _ =
Summary.declare_summary "program-tcc-table"
@@ -442,6 +442,7 @@ and solve_obligation_by_tac prg obls i tac =
true
else false
with
+ | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
| Stdpp.Exc_located(_, Refiner.FailError (_, s))
| Refiner.FailError (_, s) ->
user_err_loc (obl.obl_location, "solve_obligation", s)
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 0e987cf2..ad76bdeb 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 11047 2008-06-03 23:08:00Z msozeau $ *)
+(* $Id: subtac_pretyping.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
open Global
open Pp
@@ -117,7 +117,6 @@ let env_with_binders env isevars l =
in aux (env, []) l
let subtac_process env isevars id bl c tycon =
-(* let bl = Implicit_quantifiers.ctx_of_class_binders (vars_of_env env) cbl @ l in *)
let c = Command.abstract_constr_expr c bl in
let tycon =
match tycon with
@@ -132,12 +131,14 @@ let subtac_process env isevars id bl c tycon =
let imps = Implicit_quantifiers.implicits_of_rawterm c in
let coqc, ctyp = interp env isevars c tycon in
let evm = non_instanciated_map env isevars (evars_of !isevars) in
- evm, coqc, (match tycon with Some (None, c) -> c | _ -> ctyp), imps
+ let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
+ evm, coqc, ty, imps
open Subtac_obligations
let subtac_proof kind 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 evars, def, ty = Eterm.eterm_obligations env id !isevars evm 0 coqc coqt 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
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index afa5817f..559b6ac1 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_pretyping_F.ml 11143 2008-06-18 15:52:42Z msozeau $ *)
+(* $Id: subtac_pretyping_F.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
open Pp
open Util
@@ -246,6 +246,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
ctxtv vdef in
evar_type_fixpoint loc env isevars names ftys vdefj;
+ let ftys = Array.map (nf_evar (evars_of !isevars)) ftys in
+ let fdefs = Array.map (fun x -> nf_evar (evars_of !isevars) (j_val x)) vdefj in
let fixj = match fixkind with
| RFix (vn,i) ->
(* First, let's find the guard indexes. *)
@@ -260,11 +262,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
vn)
in
- let fixdecls = (names,ftys,Array.map j_val vdefj) in
+ let fixdecls = (names,ftys,fdefs) in
let indexes = search_guard loc env possible_indexes fixdecls in
make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
| RCoFix i ->
- let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
+ let cofix = (i,(names,ftys,fdefs)) in
(try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
make_judge (mkCoFix cofix) ftys.(i) in
inh_conv_coerce_to_tycon loc env isevars fixj tycon
@@ -273,13 +275,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
| RApp (loc,f,args) ->
- let length = List.length args in
+ let length = List.length args in
let ftycon =
- match tycon with
- None -> None
+ if length > 0 then
+ match tycon with
+ | None -> None
| Some (None, ty) -> mk_abstr_tycon length ty
| Some (Some (init, cur), ty) ->
Some (Some (length + init, length + cur), ty)
+ else tycon
in
let fj = pretype ftycon env isevars lvar f in
let floc = loc_of_rawconstr f in
@@ -291,23 +295,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
match kind_of_term resty with
| Prod (na,c1,c2) ->
- let hj = pretype (mk_tycon c1) env isevars lvar c in
+ Option.iter (fun ty -> isevars :=
+ Coercion.inh_conv_coerces_to loc env !isevars resty ty) tycon;
+ let evd, (_, _, tycon) = split_tycon loc env !isevars tycon in
+ isevars := evd;
+ let hj = pretype (mk_tycon (nf_isevar !isevars c1)) env isevars lvar c in
let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
let typ' = nf_isevar !isevars typ in
- let tycon =
- Option.map
- (fun (abs, ty) ->
- match abs with
- None ->
- isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
- (abs, ty);
- (abs, ty)
- | Some (init, cur) ->
- isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
- (abs, ty);
- (Some (init, pred cur), ty))
- tycon
- in
apply_rec env (n+1)
{ uj_val = nf_isevar !isevars value;
uj_type = nf_isevar !isevars typ' }
@@ -319,7 +313,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
(join_loc floc argloc) env (evars_of !isevars)
resj [hj]
in
- let ftycon = Option.map (lift_abstr_tycon_type (-1)) ftycon in
let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
let resj =
match kind_of_term resj.uj_val with
@@ -332,12 +325,22 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
inh_conv_coerce_to_tycon loc env isevars resj tycon
| RLambda(loc,name,k,c1,c2) ->
- let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
+ let tycon' = evd_comb1
+ (fun evd tycon ->
+ match tycon with
+ | None -> evd, tycon
+ | Some ty ->
+ let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in
+ evd, Some ty')
+ isevars tycon
+ in
+ let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon' in
let dom_valcon = valcon_of_tycon dom in
let j = pretype_type dom_valcon env isevars lvar c1 in
let var = (name,None,j.utj_val) in
let j' = pretype rng (push_rel var env) isevars lvar c2 in
- judge_of_abstraction env name j j'
+ let resj = judge_of_abstraction env name j j' in
+ inh_conv_coerce_to_tycon loc env isevars resj tycon
| RProd(loc,name,k,c1,c2) ->
let j = pretype_type empty_valcon env isevars lvar c1 in
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index 3ceea173..05fc0803 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -1,5 +1,5 @@
(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
Require Import List.
Set Implicit Arguments.
@@ -7,7 +7,7 @@ Set Implicit Arguments.
Section Accessors.
Variable A : Set.
- Program Definition myhd : forall { l : list A | length l <> 0 }, A :=
+ Program Definition myhd : forall (l : list A | length l <> 0), A :=
fun l =>
match l with
| nil => !
@@ -39,7 +39,7 @@ Section app.
Next Obligation.
intros.
- destruct_call app ; subtac_simpl.
+ destruct_call app ; program_simpl.
Defined.
Program Lemma app_id_l : forall l : list A, l = nil ++ l.
@@ -49,7 +49,7 @@ Section app.
Program Lemma app_id_r : forall l : list A, l = l ++ nil.
Proof.
- induction l ; simpl ; auto.
+ induction l ; simpl in * ; auto.
rewrite <- IHl ; auto.
Qed.
@@ -70,16 +70,24 @@ Section Nth.
Next Obligation.
Proof.
- intros.
- inversion H.
+ simpl in *. auto with arith.
Defined.
+ Next Obligation.
+ Proof.
+ inversion H.
+ Qed.
+
Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A :=
match l, n with
| hd :: _, 0 => hd
| _ :: tl, S n' => nth' tl n'
| nil, _ => !
end.
+ Next Obligation.
+ Proof.
+ simpl in *. auto with arith.
+ Defined.
Next Obligation.
Proof.
diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v
index 87ab47d6..2e17959c 100644
--- a/contrib/subtac/test/take.v
+++ b/contrib/subtac/test/take.v
@@ -1,9 +1,12 @@
(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
Require Import JMeq.
Require Import List.
-Require Import Coq.subtac.Utils.
+Require Import Program.
Set Implicit Arguments.
+Obligations Tactic := idtac.
+
+Print cons.
Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
match n with
@@ -16,21 +19,14 @@ Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct
end.
Require Import Omega.
-
+Solve All Obligations.
Next Obligation.
- intros.
- simpl in l0.
- apply le_S_n ; exact l0.
-Defined.
-
-Next Obligation.
- intros.
- destruct_call take ; subtac_simpl.
+ destruct_call take ; program_simpl.
Defined.
Next Obligation.
intros.
- inversion l0.
+ inversion H.
Defined.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 07:50:34 +0000