diff options
| -rw-r--r-- | pretyping/termops.ml | 8 | ||||
| -rw-r--r-- | pretyping/termops.mli | 1 | ||||
| -rw-r--r-- | proofs/logic.ml | 11 | ||||
| -rw-r--r-- | test-suite/output/Fixpoint.out | 2 | ||||
| -rw-r--r-- | test-suite/success/apply.v | 9 | ||||
| -rw-r--r-- | toplevel/discharge.ml | 2 |
6 files changed, 20 insertions, 13 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index a81f68b79..124637e13 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -160,15 +160,19 @@ let new_Type_sort () = Type (new_univ ()) (* This refreshes universes in types; works only for inferred types (i.e. for types of the form (x1:A1)...(xn:An)B with B a sort or an atom in head normal form) *) -let refresh_universes t = +let refresh_universes_gen strict t = let modified = ref false in let rec refresh t = match kind_of_term t with - | Sort (Type u) when u <> Univ.lower_univ -> modified := true; new_Type () + | Sort (Type u) when strict or u <> Univ.lower_univ -> + modified := true; new_Type () | Prod (na,u,v) -> mkProd (na,u,refresh v) | _ -> t in let t' = refresh t in if !modified then t' else t +let refresh_universes = refresh_universes_gen false +let refresh_universes_strict = refresh_universes_gen true + let new_sort_in_family = function | InProp -> prop_sort | InSet -> set_sort diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 64edcd2e3..ded85464e 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -21,6 +21,7 @@ val new_sort_in_family : sorts_family -> sorts val new_Type : unit -> types val new_Type_sort : unit -> sorts val refresh_universes : types -> types +val refresh_universes_strict : types -> types (* printers *) val print_sort : sorts -> std_ppcmds diff --git a/proofs/logic.ml b/proofs/logic.ml index 24de605ac..d61fe21de 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -51,8 +51,9 @@ let rec catchable_exception = function | RefinerError _ | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) (* unification errors *) - | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _|NoOccurrenceFound _| - CannotUnifyBindingType _|NotClean _)) -> true + | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ + |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ + |CannotFindWellTypedAbstraction _)) -> true | _ -> false (* Tells if the refiner should check that the submitted rules do not @@ -277,8 +278,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty) = 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 *) -> + | Ind _ | Const _ + when not (array_exists occur_meta l) (* we could be finer *) + & (isInd f or Heads.has_inductive_head env f) + -> (* Sort-polymorphism of definition and inductive types *) goalacc, type_of_global_reference_knowing_parameters env sigma f l diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index cbb387ce9..f4270d3de 100644 --- a/test-suite/output/Fixpoint.out +++ b/test-suite/output/Fixpoint.out @@ -22,4 +22,4 @@ fix even_pos_odd_pos 2 destruct H. apply even_pos_odd_pos in H. omega. - + diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index e3fed09e7..deeab4cb6 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -175,12 +175,11 @@ Theorem t : r true false. apply ax with (R := r). Qed. +(* Check verification of type at unification (submitted by Stéphane Lengrand): + without verification, the first "apply" works what leads to the incorrect + instantiation of x by Prop *) -(* Check verification of type at unification (Submitted by Stéphane Lengrand) - (without verification, the first "apply" works which leads to wrongly - instantiate x by Prop) *) - -Theorem t: ~(forall x:Prop, ~x). +Theorem u : ~(forall x:Prop, ~x). unfold not. intro. eapply H. diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 3f1b4c2c2..dfed4a3be 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -73,7 +73,7 @@ let process_inductive sechyps modlist mib = let inds = array_map_to_list (fun mip -> - let arity = expmod_constr modlist (Termops.refresh_universes (Inductive.type_of_inductive (Global.env()) (mib,mip))) in + let arity = expmod_constr modlist (Termops.refresh_universes_strict (Inductive.type_of_inductive (Global.env()) (mib,mip))) in let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in (mip.mind_typename, arity, |