summaryrefslogtreecommitdiff
path: root/proofs/logic.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/logic.ml')
-rw-r--r--proofs/logic.ml63
1 files changed, 40 insertions, 23 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml
index ffbc0d56..e40d1232 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: logic.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
+(* $Id: logic.ml 9323 2006-10-30 23:05:29Z herbelin $ *)
open Pp
open Util
@@ -80,15 +80,15 @@ let clear_hyps ids gl =
error (string_of_id id'^
" is used in hypothesis "^string_of_id id))
(global_vars_set_of_decl env d) in
- clear_hyps ids fcheck gl.evar_hyps in
+ clear_hyps ids fcheck gl.evar_hyps in
let ncl = gl.evar_concl in
- if !check && cleared_ids<>[] then
- Idset.iter
- (fun id' ->
- if List.mem id' cleared_ids then
- error (string_of_id id'^" is used in conclusion"))
- (global_vars_set env ncl);
- mk_goal nhyps ncl
+ if !check && cleared_ids<>[] then
+ Idset.iter
+ (fun id' ->
+ if List.mem id' cleared_ids then
+ error (string_of_id id'^" is used in conclusion"))
+ (global_vars_set_drop_evar env ncl);
+ mk_goal nhyps ncl gl.evar_extra
(* The ClearBody tactic *)
@@ -155,7 +155,7 @@ let split_sign hfrom hto l =
else
splitrec (d::left) (toleft or (hyp = hto)) right
in
- splitrec [] false l
+ splitrec [] false l
let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
let env = Global.env() in
@@ -214,19 +214,25 @@ let check_forward_dependencies id tail =
^ (string_of_id id')))
tail
+let check_goal_dependency id cl =
+ let env = Global.env() in
+ if Idset.mem id (global_vars_set_drop_evar env cl) then
+ error (string_of_id id^" is used in conclusion")
let rename_hyp id1 id2 sign =
apply_to_hyp_and_dependent_on sign id1
(fun (_,b,t) _ -> (id2,b,t))
(fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
-let replace_hyp sign id d =
+let replace_hyp sign id d cl =
+ if !check then
+ check_goal_dependency id cl;
apply_to_hyp sign id
(fun sign _ tail ->
- if !check then
- (check_backward_dependencies sign d;
- check_forward_dependencies id tail);
- d)
+ if !check then
+ (check_backward_dependencies sign d;
+ check_forward_dependencies id tail);
+ d)
(* why we dont check that id does not appear in tail ??? *)
let insert_after_hyp sign id d =
@@ -264,6 +270,7 @@ let goal_type_of env sigma c =
let rec mk_refgoals sigma goal goalacc conclty trm =
let env = evar_env goal in
let hyps = goal.evar_hyps in
+ let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
(*
if not (occur_meta trm) then
let t'ty = (unsafe_machine env sigma trm).uj_type in
@@ -284,9 +291,14 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
| App (f,l) ->
let (acc',hdty) =
- if isInd f & not (array_exists occur_meta l) (* we could be finer *)
- then (goalacc,type_of_inductive_knowing_parameters env sigma (destInd f) l)
- else mk_hdgoals sigma goal goalacc f
+ match kind_of_term f with
+ | (Ind _ (* needed if defs in Type are polymorphic: | Const _*))
+ when not (array_exists occur_meta l) (* we could be finer *) ->
+ (* Sort-polymorphism of definition and inductive types *)
+ goalacc,
+ type_of_global_reference_knowing_parameters env sigma f l
+ | _ ->
+ mk_hdgoals sigma goal goalacc f
in
let (acc'',conclty') =
mk_arggoals sigma goal acc' hdty (Array.to_list l) in
@@ -315,6 +327,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
and mk_hdgoals sigma goal goalacc trm =
let env = evar_env goal in
let hyps = goal.evar_hyps in
+ let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
match kind_of_term trm with
| Cast (c,_, ty) when isMeta c ->
check_typability env sigma ty;
@@ -326,8 +339,10 @@ and mk_hdgoals sigma goal goalacc trm =
| App (f,l) ->
let (acc',hdty) =
- if isInd f & not (array_exists occur_meta l) (* we could be finer *)
- then (goalacc,type_of_inductive_knowing_parameters env sigma (destInd f) l)
+ if isInd f or isConst f
+ & not (array_exists occur_meta l) (* we could be finer *)
+ then
+ (goalacc,type_of_global_reference_knowing_parameters env sigma f l)
else mk_hdgoals sigma goal goalacc f
in
mk_arggoals sigma goal acc' hdty (Array.to_list l)
@@ -392,6 +407,7 @@ let prim_refiner r sigma goal =
let env = evar_env goal in
let sign = goal.evar_hyps in
let cl = goal.evar_concl in
+ let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
match r with
(* Logical rules *)
| Intro id ->
@@ -416,12 +432,12 @@ let prim_refiner r sigma goal =
(match kind_of_term (strip_outer_cast cl) with
| Prod (_,c1,b) ->
if occur_meta c1 then error_use_instantiate();
- let sign' = replace_hyp sign id (id,None,c1) in
+ let sign' = replace_hyp sign id (id,None,c1) cl in
let sg = mk_goal sign' (subst1 (mkVar id) b) in
[sg]
| LetIn (_,c1,t1,b) ->
if occur_meta c1 then error_use_instantiate();
- let sign' = replace_hyp sign id (id,Some c1,t1) in
+ let sign' = replace_hyp sign id (id,Some c1,t1) cl in
let sg = mk_goal sign' (subst1 (mkVar id) b) in
[sg]
| _ ->
@@ -474,7 +490,8 @@ let prim_refiner r sigma goal =
let _ = find_coinductive env sigma b in ()
with Not_found ->
error ("All methods must construct elements " ^
- "in coinductive types")
+ "in coinductiv-> goal
+e types")
in
let all = (f,cl)::others in
List.iter (fun (_,c) -> check_is_coind env c) all;