Skip to content
Browse files

- Add externalisation code for universe level instances.

- Support for polymorphism in pretyping/command and proofs/proofview etc.
  Needed wrapping of [fresh_.._instance] through the evar_map, which
  contains the local state of universes during type-checking.
- Correct the inductive scheme generation to support polymorphism as well.
- Have to review kernel code for correctness, and especially rework the
  computation of universe constraints for inductives.
Stops somewhat later in Logic.v
  • Loading branch information...
1 parent 9100abc commit f9e0358e3206efe39578c9a0cdd2bfd682d5fb2e @mattam82 mattam82 committed Oct 16, 2012
Showing with 458 additions and 271 deletions.
  1. +2 −2 grammar/q_constr.ml4
  2. +4 −3 grammar/q_coqast.ml4
  3. +8 −8 interp/constrexpr_ops.ml
  4. +24 −22 interp/constrextern.ml
  5. +18 −17 interp/constrintern.ml
  6. +4 −2 interp/constrintern.mli
  7. +9 −9 interp/implicit_quantifiers.ml
  8. +4 −4 interp/notation.ml
  9. +6 −6 interp/notation_ops.ml
  10. +4 −4 interp/topconstr.ml
  11. +2 −2 intf/constrexpr.mli
  12. +1 −1 intf/glob_term.mli
  13. +1 −1 kernel/indtypes.ml
  14. +10 −1 kernel/inductive.ml
  15. +3 −0 kernel/inductive.mli
  16. +3 −0 kernel/sign.ml
  17. +2 −0 kernel/sign.mli
  18. +8 −4 kernel/term.ml
  19. +2 −2 kernel/typeops.ml
  20. +1 −1 kernel/typeops.mli
  21. +13 −0 kernel/univ.ml
  22. +4 −0 kernel/univ.mli
  23. +2 −2 parsing/egramcoq.ml
  24. +7 −7 parsing/g_constr.ml4
  25. +1 −1 parsing/g_tactic.ml4
  26. +3 −3 parsing/g_xml.ml4
  27. +2 −2 plugins/decl_mode/decl_interp.ml
  28. +2 −2 plugins/decl_mode/g_decl_mode.ml4
  29. +1 −1 pretyping/cases.ml
  30. +5 −5 pretyping/detyping.ml
  31. +14 −10 pretyping/evarconv.ml
  32. +19 −0 pretyping/evarutil.ml
  33. +10 −0 pretyping/evarutil.mli
  34. +15 −0 pretyping/evd.ml
  35. +8 −0 pretyping/evd.mli
  36. +5 −5 pretyping/glob_ops.ml
  37. +9 −9 pretyping/indrec.ml
  38. +1 −1 pretyping/patternops.ml
  39. +21 −10 pretyping/pretyping.ml
  40. +14 −8 printing/ppconstr.ml
  41. +4 −2 proofs/pfedit.ml
  42. +4 −3 proofs/pfedit.mli
  43. +2 −2 proofs/proof.ml
  44. +2 −2 proofs/proof.mli
  45. +6 −7 proofs/proof_global.ml
  46. +1 −1 proofs/proof_global.mli
  47. +4 −2 proofs/proofview.ml
  48. +2 −2 proofs/proofview.mli
  49. +10 −4 tactics/elimschemes.ml
  50. +20 −9 tactics/eqschemes.ml
  51. +6 −4 tactics/eqschemes.mli
  52. +1 −1 tactics/leminv.ml
  53. +4 −4 tactics/rewrite.ml4
  54. +4 −4 tactics/tacintern.ml
  55. +1 −1 tactics/tacinterp.ml
  56. +2 −1 tactics/tactics.ml
  57. +25 −6 theories/Init/Logic.v
  58. +11 −8 toplevel/auto_ind_decl.ml
  59. +4 −4 toplevel/auto_ind_decl.mli
  60. +2 −2 toplevel/classes.ml
  61. +7 −5 toplevel/command.ml
  62. +19 −11 toplevel/ind_tables.ml
  63. +9 −2 toplevel/ind_tables.mli
  64. +13 −12 toplevel/indschemes.ml
  65. +12 −8 toplevel/lemmas.ml
  66. +3 −2 toplevel/lemmas.mli
  67. +2 −2 toplevel/metasyntax.ml
  68. +3 −2 toplevel/obligations.ml
  69. +3 −3 toplevel/whelp.ml4
View
4 grammar/q_constr.ml4
@@ -18,7 +18,7 @@ let dloc = <:expr< Loc.ghost >>
let apply_ref f l =
<:expr<
- Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$), $mlexpr_of_list (fun x -> x) l$)
+ Glob_term.GApp ($dloc$, Glob_term.GRef ($dloc$, Lazy.force $f$, None), $mlexpr_of_list (fun x -> x) l$)
>>
EXTEND
@@ -74,7 +74,7 @@ EXTEND
| "?"; id = ident -> <:expr< Glob_term.GPatVar($dloc$,(False,$id$)) >>
| "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" ->
apply_ref <:expr< coq_sumbool_ref >> [c1;c2]
- | "%"; e = string -> <:expr< Glob_term.GRef ($dloc$,Lazy.force $lid:e$) >>
+ | "%"; e = string -> <:expr< Glob_term.GRef ($dloc$,Lazy.force $lid:e$, None) >>
| c = match_constr -> c
| "("; c = constr LEVEL "200"; ")" -> c ] ]
;
View
7 grammar/q_coqast.ml4
@@ -139,10 +139,10 @@ let mlexpr_of_binder_kind = function
$mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >>
let rec mlexpr_of_constr = function
- | Constrexpr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->
+ | Constrexpr.CRef (Libnames.Ident (loc,id),_) when is_meta (string_of_id id) ->
let loc = of_coqloc loc in
anti loc (string_of_id id)
- | Constrexpr.CRef r -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ >>
+ | Constrexpr.CRef (r,n) -> <:expr< Constrexpr.CRef $mlexpr_of_reference r$ None >>
| Constrexpr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
| Constrexpr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
| Constrexpr.CProdN (loc,l,a) ->
@@ -153,8 +153,9 @@ let rec mlexpr_of_constr = function
let loc = of_coqloc loc in
<:expr< Constrexpr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
| Constrexpr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
- | Constrexpr.CAppExpl (loc,a,l) ->
+ | Constrexpr.CAppExpl (loc,(p,r,us),l) ->
let loc = of_coqloc loc in
+ let a = (p,r) in
<:expr< Constrexpr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
| Constrexpr.CApp (loc,a,l) ->
let loc = of_coqloc loc in
View
16 interp/constrexpr_ops.ml
@@ -41,8 +41,8 @@ let names_of_local_binders bl =
(* Functions on constr_expr *)
let constr_loc = function
- | CRef (Ident (loc,_)) -> loc
- | CRef (Qualid (loc,_)) -> loc
+ | CRef (Ident (loc,_),_) -> loc
+ | CRef (Qualid (loc,_),_) -> loc
| CFix (loc,_,_) -> loc
| CCoFix (loc,_,_) -> loc
| CProdN (loc,_,_) -> loc
@@ -92,8 +92,8 @@ let local_binders_loc bll = match bll with
(** Pseudo-constructors *)
-let mkIdentC id = CRef (Ident (Loc.ghost, id))
-let mkRefC r = CRef r
+let mkIdentC id = CRef (Ident (Loc.ghost, id),None)
+let mkRefC r = CRef (r,None)
let mkCastC (a,k) = CCast (Loc.ghost,a,k)
let mkLambdaC (idl,bk,a,b) = CLambdaN (Loc.ghost,[idl,bk,a],b)
let mkLetInC (id,a,b) = CLetIn (Loc.ghost,id,a,b)
@@ -144,13 +144,13 @@ let coerce_reference_to_id = function
str "This expression should be a simple identifier.")
let coerce_to_id = function
- | CRef (Ident (loc,id)) -> (loc,id)
+ | CRef (Ident (loc,id),_) -> (loc,id)
| a -> Errors.user_err_loc
(constr_loc a,"coerce_to_id",
str "This expression should be a simple identifier.")
let coerce_to_name = function
- | CRef (Ident (loc,id)) -> (loc,Name id)
+ | CRef (Ident (loc,id),_) -> (loc,Name id)
| CHole (loc,_) -> (loc,Anonymous)
| a -> Errors.user_err_loc
(constr_loc a,"coerce_to_name",
@@ -159,10 +159,10 @@ let coerce_to_name = function
let rec raw_cases_pattern_expr_of_glob_constr looked_for = function
| GVar (loc,id) -> RCPatAtom (loc,Some id)
| GHole (loc,_) -> RCPatAtom (loc,None)
- | GRef (loc,g) ->
+ | GRef (loc,g,_) ->
looked_for g;
RCPatCstr (loc, g,[],[])
- | GApp (loc,GRef (_,g),l) ->
+ | GApp (loc,GRef (_,g,_),l) ->
looked_for g;
RCPatCstr (loc, g,[],List.map (raw_cases_pattern_expr_of_glob_constr looked_for) l)
| _ -> raise Not_found
View
46 interp/constrextern.ml
@@ -189,7 +189,7 @@ let same_id (id1, c1) (id2, c2) =
let rec check_same_type ty1 ty2 =
match ty1, ty2 with
- | CRef r1, CRef r2 -> check_same_ref r1 r2
+ | CRef (r1,_), CRef (r2,_) -> check_same_ref r1 r2
| CFix(_,id1,fl1), CFix(_,id2,fl2) when eq_located id_eq id1 id2 ->
List.iter2 (fun ((_, id1),i1,bl1,a1,b1) ((_, id2),i2,bl2,a2,b2) ->
if not (id_eq id1 id2) || not (same_id i1 i2) then failwith "not same fix";
@@ -213,7 +213,8 @@ let rec check_same_type ty1 ty2 =
| CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when name_eq na1 na2 ->
check_same_type a1 a2;
check_same_type b1 b2
- | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) when Option.Misc.compare Int.equal proj1 proj2 ->
+ | CAppExpl(_,(proj1,r1,_),al1), CAppExpl(_,(proj2,r2,_),al2) when
+ Option.Misc.compare Int.equal proj1 proj2 ->
check_same_ref r1 r2;
List.iter2 check_same_type al1 al2
| CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) ->
@@ -582,8 +583,8 @@ let explicitize loc inctx impl (cf,f) args =
match is_projection (List.length args) cf with
| Some i as ip ->
if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then
- let f' = match f with CRef f -> f | _ -> assert false in
- CAppExpl (loc,(ip,f'),args)
+ let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in
+ CAppExpl (loc,(ip,f',us),args)
else
let (args1,args2) = List.chop i args in
let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in
@@ -594,26 +595,26 @@ let explicitize loc inctx impl (cf,f) args =
let args = exprec 1 (args,impl) in
if List.is_empty args then f else CApp (loc, (None, f), args)
-let extern_global loc impl f =
+let extern_global loc impl f us =
if not !Constrintern.parsing_explicit &&
not (List.is_empty impl) && List.for_all is_status_implicit impl
then
- CAppExpl (loc, (None, f), [])
+ CAppExpl (loc, (None, f, us), [])
else
- CRef f
+ CRef (f,us)
-let extern_app loc inctx impl (cf,f) args =
+let extern_app loc inctx impl (cf,f) us args =
if List.is_empty args then
(* If coming from a notation "Notation a := @b" *)
- CAppExpl (loc, (None, f), [])
+ CAppExpl (loc, (None, f, us), [])
else if not !Constrintern.parsing_explicit &&
((!Flags.raw_print ||
(!print_implicits & not !print_implicits_explicit_args)) &
List.exists is_status_implicit impl)
then
- CAppExpl (loc, (is_projection (List.length args) cf, f), args)
+ CAppExpl (loc, (is_projection (List.length args) cf,f,us), args)
else
- explicitize loc inctx impl (cf,CRef f) args
+ explicitize loc inctx impl (cf,CRef (f,us)) args
let rec extern_args extern scopes env args subscopes =
match args with
@@ -625,7 +626,7 @@ let rec extern_args extern scopes env args subscopes =
extern argscopes env a :: extern_args extern scopes env args subscopes
let rec remove_coercions inctx = function
- | GApp (loc,GRef (_,r),args) as c
+ | GApp (loc,GRef (_,r,_),args) as c
when not (!Flags.raw_print or !print_coercions)
->
let nargs = List.length args in
@@ -693,11 +694,11 @@ let rec extern inctx scopes vars r =
if !Flags.raw_print or !print_no_symbol then raise No_match;
extern_symbol scopes vars r'' (uninterp_notations r'')
with No_match -> match r' with
- | GRef (loc,ref) ->
+ | GRef (loc,ref,us) ->
extern_global loc (select_stronger_impargs (implicits_of_global ref))
- (extern_reference loc vars ref)
+ (extern_reference loc vars ref) us
- | GVar (loc,id) -> CRef (Ident (loc,id))
+ | GVar (loc,id) -> CRef (Ident (loc,id),None)
| GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None)
@@ -709,7 +710,7 @@ let rec extern inctx scopes vars r =
| GApp (loc,f,args) ->
(match f with
- | GRef (rloc,ref) ->
+ | GRef (rloc,ref,us) ->
let subscopes = find_arguments_scope ref in
let args =
extern_args (extern true) (snd scopes) vars args subscopes in
@@ -748,14 +749,15 @@ let rec extern inctx scopes vars r =
| [] -> raise No_match
(* we give up since the constructor is not complete *)
| head :: tail -> ip q locs' tail
- ((extern_reference loc Idset.empty (ConstRef c), head) :: acc)
+ ((extern_reference loc Idset.empty (ConstRef c), head)
+ :: acc)
in
CRecord (loc, None, List.rev (ip projs locals args []))
with
| Not_found | No_match | Exit ->
extern_app loc inctx
(select_stronger_impargs (implicits_of_global ref))
- (Some ref,extern_reference rloc vars ref) args
+ (Some ref,extern_reference rloc vars ref) us args
end
| _ ->
explicitize loc inctx [] (None,sub_extern false scopes vars f)
@@ -918,7 +920,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
let args1, args2 = List.chop n args in
let subscopes, impls =
match f with
- | GRef (_,ref) ->
+ | GRef (_,ref,us) ->
let subscopes =
try List.skipn n (find_arguments_scope ref) with _ -> [] in
let impls =
@@ -931,7 +933,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
[], [] in
(if Int.equal n 0 then f else GApp (Loc.ghost,f,args1)),
args2, subscopes, impls
- | GApp (_,(GRef (_,ref) as f),args), None ->
+ | GApp (_,(GRef (_,ref,us) as f),args), None ->
let subscopes = find_arguments_scope ref in
let impls =
select_impargs_size
@@ -972,7 +974,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
List.map (fun (c,(scopt,scl)) ->
extern true (scopt,scl@scopes) vars c, None)
terms in
- let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in
+ let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn),None) in
if List.is_empty l then a else CApp (loc,(None,a),l) in
if List.is_empty args then e
else
@@ -1035,7 +1037,7 @@ let any_any_branch =
(loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole))
let rec glob_of_pat env = function
- | PRef ref -> GRef (loc,ref)
+ | PRef ref -> GRef (loc,ref,None)
| PVar id -> GVar (loc,id)
| PEvar (n,l) -> GEvar (loc,n,Some (Array.map_to_list (glob_of_pat env) l))
| PRel n ->
View
35 interp/constrintern.ml
@@ -297,7 +297,7 @@ let reset_tmp_scope env = {env with tmp_scope = None}
let set_scope env = function
| CastConv (GSort _) -> set_type_scope env
- | CastConv (GRef (_,ref) | GApp (_,GRef (_,ref),_)) ->
+ | CastConv (GRef (_,ref,_) | GApp (_,GRef (_,ref,_),_)) ->
{env with tmp_scope = compute_scope_of_global ref}
| _ -> env
@@ -406,7 +406,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
let name =
let id =
match ty with
- | CApp (_, (_, CRef (Ident (loc,id))), _) -> id
+ | CApp (_, (_, CRef (Ident (loc,id),_)), _) -> id
| _ -> id_of_string "H"
in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
in Name name
@@ -609,7 +609,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
try
let ty,expl_impls,impls,argsc = Idmap.find id genv.impls in
let expl_impls = List.map
- (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in
+ (fun id -> CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
let tys = string_of_ty ty in
Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
GVar (loc,id), make_implicits_list impls, argsc, expl_impls
@@ -644,15 +644,15 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
- GRef (loc, ref), impls, scopes, []
+ GRef (loc, ref, None), impls, scopes, []
with _ ->
(* [id] a goal variable *)
GVar (loc,id), [], [], []
let find_appl_head_data = function
- | GRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
- | GApp (_,GRef (_,ref),l) as x
- when l != [] && Flags.version_strictly_greater Flags.V8_2 ->
+ | GRef (_,ref,_) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
+ | GApp (_,GRef (_,ref,_),l) as x
+ when l != [] & Flags.version_strictly_greater Flags.V8_2 ->
let n = List.length l in
x,List.map (drop_first_implicits n) (implicits_of_global ref),
List.skipn_at_least n (find_arguments_scope ref),[]
@@ -686,7 +686,7 @@ let intern_reference ref =
let intern_qualid loc qid intern env lvar args =
match intern_extended_global_of_qualid (loc,qid) with
| TrueGlobal ref ->
- GRef (loc, ref), args
+ GRef (loc, ref, None), args
| SynDef sp ->
let (ids,c) = Syntax_def.search_syntactic_definition sp in
let nids = List.length ids in
@@ -699,7 +699,7 @@ let intern_qualid loc qid intern env lvar args =
(* Rule out section vars since these should have been found by intern_var *)
let intern_non_secvar_qualid loc qid intern env lvar args =
match intern_qualid loc qid intern env lvar args with
- | GRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
+ | GRef (loc, VarRef id, None),_ -> error_global_not_found_loc loc qid
| r -> r
let intern_applied_reference intern env namedctx lvar args = function
@@ -1209,7 +1209,7 @@ let merge_impargs l args =
let check_projection isproj nargs r =
match (r,isproj) with
- | GRef (loc, ref), Some _ ->
+ | GRef (loc, ref, _), Some _ ->
(try
let n = Recordops.find_projection_nparams ref + 1 in
if not (Int.equal nargs n) then
@@ -1224,7 +1224,7 @@ let get_implicit_name n imps =
Some (Impargs.name_of_implicit (List.nth imps (n-1)))
let set_hole_implicit i b = function
- | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b))
+ | GRef (loc,r,_) | GApp (_,GRef (loc,r,_),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b))
| GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b))
| _ -> anomaly "Only refs have implicits"
@@ -1270,7 +1270,7 @@ let extract_explicit_arg imps args =
let internalize sigma globalenv env allow_patvar lvar c =
let rec intern env = function
- | CRef ref as x ->
+ | CRef (ref,us) as x ->
let (c,imp,subscopes,l),_ =
intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in
(match intern_impargs c env imp subscopes l with
@@ -1368,7 +1368,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
| CDelimiters (loc, key, e) ->
intern {env with tmp_scope = None;
scopes = find_delimiters_scope loc key :: env.scopes} e
- | CAppExpl (loc, (isproj,ref), args) ->
+ | CAppExpl (loc, (isproj,ref,us), args) ->
let (f,_,args_scopes,_),args =
let args = List.map (fun a -> (a,None)) args in
intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref in
@@ -1383,7 +1383,8 @@ let internalize sigma globalenv env allow_patvar lvar c =
| _ -> isproj,f,args in
let (c,impargs,args_scopes,l),args =
match f with
- | CRef ref -> intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref
+ | CRef (ref,us) ->
+ intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref
| CNotation (loc,ntn,([],[],[])) ->
let c = intern_notation intern env lvar loc ntn ([],[],[]) in
find_appl_head_data c, args
@@ -1405,7 +1406,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
| None -> user_err_loc (loc, "intern", str"No constructor inference.")
| Some (n, constrname, args) ->
let pars = List.make n (CHole (loc, None)) in
- let app = CAppExpl (loc, (None, constrname), List.rev_append pars args) in
+ let app = CAppExpl (loc, (None, constrname,None), List.rev_append pars args) in
intern env app
end
| CCases (loc, sty, rtnpo, tms, eqns) ->
@@ -1512,7 +1513,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
(* the "as" part *)
let extra_id,na = match tm', na with
| GVar (loc,id), None when Idset.mem id env.ids -> Some id,(loc,Name id)
- | GRef (loc, VarRef id), None -> Some id,(loc,Name id)
+ | GRef (loc, VarRef id,_), None -> Some id,(loc,Name id)
| _, None -> None,(Loc.ghost,Anonymous)
| _, Some (loc,na) -> None,(loc,na) in
(* the "in" part *)
@@ -1686,7 +1687,7 @@ let interp_open_constr_patvar sigma env c =
| GPatVar (loc,(_,id)) ->
( try Gmap.find id !evars
with Not_found ->
- let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in
+ let ev = Evarutil.e_new_type_evar sigma env in
let ev = Evarutil.e_new_evar sigma env ev in
let rev = GEvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in
evars := Gmap.add id rev !evars;
View
6 interp/constrintern.mli
@@ -160,10 +160,12 @@ val interp_context_gen : (env -> glob_constr -> types) ->
evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
val interp_context : ?global_level:bool -> ?impl_env:internalization_env ->
- evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+ evar_map -> env -> local_binder list ->
+ internalization_env * ((env * rel_context) * Impargs.manual_implicits)
val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env ->
- evar_map ref -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+ evar_map ref -> env -> local_binder list ->
+ internalization_env * ((env * rel_context) * Impargs.manual_implicits)
(** Locating references of constructions, possibly via a syntactic definition
(these functions do not modify the glob file) *)
View
18 interp/implicit_quantifiers.ml
@@ -104,8 +104,8 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
else l
in
let rec aux bdvars l c = match c with
- | CRef (Ident (loc,id)) -> found loc id bdvars l
- | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [], [])) when not (Idset.mem id bdvars) ->
+ | CRef (Ident (loc,id),_) -> found loc id bdvars l
+ | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id),_) :: _, [], [])) when not (Idset.mem id bdvars) ->
Topconstr.fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
| c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
in aux bound l c
@@ -255,19 +255,19 @@ let combine_params avoid fn applied needed =
let combine_params_freevar =
fun avoid (_, (na, _, _)) ->
let id' = next_name_away_from na avoid in
- (CRef (Ident (Loc.ghost, id')), Idset.add id' avoid)
+ (CRef (Ident (Loc.ghost, id'),None), Idset.add id' avoid)
let destClassApp cl =
match cl with
- | CApp (loc, (None, CRef ref), l) -> loc, ref, List.map fst l
- | CAppExpl (loc, (None, ref), l) -> loc, ref, l
- | CRef ref -> loc_of_reference ref, ref, []
+ | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, List.map fst l
+ | CAppExpl (loc, (None, ref,_), l) -> loc, ref, l
+ | CRef (ref,_) -> loc_of_reference ref, ref, []
| _ -> raise Not_found
let destClassAppExpl cl =
match cl with
- | CApp (loc, (None, CRef ref), l) -> loc, ref, l
- | CRef ref -> loc_of_reference ref, ref, []
+ | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, l
+ | CRef (ref,_) -> loc_of_reference ref, ref, []
| _ -> raise Not_found
let implicit_application env ?(allow_partial=true) f ty =
@@ -299,7 +299,7 @@ let implicit_application env ?(allow_partial=true) f ty =
end;
let pars = List.rev (List.combine ci rd) in
let args, avoid = combine_params avoid f par pars in
- CAppExpl (loc, (None, id), args), avoid
+ CAppExpl (loc, (None, id, None), args), avoid
in c, avoid
let implicits_of_glob_constr ?(with_products=true) l =
View
8 interp/notation.ml
@@ -220,12 +220,12 @@ let notations_key_table = ref Gmapl.empty
let prim_token_key_table = Hashtbl.create 7
let glob_prim_constr_key = function
- | GApp (_,GRef (_,ref),_) | GRef (_,ref) -> RefKey (canonical_gr ref)
+ | GApp (_,GRef (_,ref,_),_) | GRef (_,ref,_) -> RefKey (canonical_gr ref)
| _ -> Oth
let glob_constr_keys = function
- | GApp (_,GRef (_,ref),_) -> [RefKey (canonical_gr ref); Oth]
- | GRef (_,ref) -> [RefKey (canonical_gr ref)]
+ | GApp (_,GRef (_,ref,_),_) -> [RefKey (canonical_gr ref); Oth]
+ | GRef (_,ref,_) -> [RefKey (canonical_gr ref)]
| _ -> [Oth]
let cases_pattern_key = function
@@ -454,7 +454,7 @@ let uninterp_prim_token_ind_pattern ind args =
if not b then raise Notation_ops.No_match;
let args' = List.map
(fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in
- let ref = GRef (Loc.ghost,ref) in
+ let ref = GRef (Loc.ghost,ref,None) in
match numpr (GApp (Loc.ghost,ref,args')) with
| None -> raise Notation_ops.No_match
| Some n -> (sc,n)
View
12 interp/notation_ops.ml
@@ -106,7 +106,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
| NSort x -> GSort (loc,x)
| NHole x -> GHole (loc,x)
| NPatVar n -> GPatVar (loc,(false,n))
- | NRef x -> GRef (loc,x)
+ | NRef x -> GRef (loc,x,None)
let glob_constr_of_notation_constr loc x =
let rec aux () x =
@@ -146,15 +146,15 @@ let split_at_recursive_part c =
let on_true_do b f c = if b then (f c; b) else b
let compare_glob_constr f add t1 t2 = match t1,t2 with
- | GRef (_,r1), GRef (_,r2) -> eq_gr r1 r2
+ | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2
| GVar (_,v1), GVar (_,v2) -> on_true_do (id_eq v1 v2) add (Name v1)
- | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
+ | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 & List.for_all2eq f l1 l2
| GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
when name_eq na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
on_true_do (f ty1 ty2 & f c1 c2) add na1
| GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2)
when name_eq na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
- on_true_do (f ty1 ty2 & f c1 c2) add na1
+ on_true_do (f ty1 ty2 & f c1 c2) add na1
| GHole _, GHole _ -> true
| GSort (_,s1), GSort (_,s2) -> glob_sort_eq s1 s2
| GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when name_eq na1 na2 ->
@@ -288,7 +288,7 @@ let notation_constr_and_vars_of_glob_constr a =
| GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
| GSort (_,s) -> NSort s
| GHole (_,w) -> NHole w
- | GRef (_,r) -> NRef r
+ | GRef (_,r,_) -> NRef r
| GPatVar (_,(_,n)) -> NPatVar n
| GEvar _ ->
error "Existential variables not allowed in notations."
@@ -635,7 +635,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
(* Matching compositionally *)
| GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma
- | GRef (_,r1), NRef r2 when (eq_gr r1 r2) -> sigma
+ | GRef (_,r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
| GPatVar (_,(_,n1)), NPatVar n2 when id_eq n1 n2 -> sigma
| GApp (loc,f1,l1), NApp (f2,l2) ->
let n1 = List.length l1 and n2 = List.length l2 in
View
8 interp/topconstr.ml
@@ -101,7 +101,7 @@ let rec fold_local_binders g f n acc b = function
f n acc b
let fold_constr_expr_with_binders g f n acc = function
- | CAppExpl (loc,(_,_),l) -> List.fold_left (f n) acc l
+ | CAppExpl (loc,(_,_,_),l) -> List.fold_left (f n) acc l
| CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
| CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l
| CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a]
@@ -141,7 +141,7 @@ let fold_constr_expr_with_binders g f n acc = function
let free_vars_of_constr_expr c =
let rec aux bdvars l = function
- | CRef (Ident (_,id)) -> if List.mem id bdvars then l else Idset.add id l
+ | CRef (Ident (_,id),None) -> if List.mem id bdvars then l else Idset.add id l
| c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
in aux [] Idset.empty c
@@ -250,8 +250,8 @@ let map_constr_expr_with_binders g f e = function
(* Used in constrintern *)
let rec replace_vars_constr_expr l = function
- | CRef (Ident (loc,id)) as x ->
- (try CRef (Ident (loc,List.assoc id l)) with Not_found -> x)
+ | CRef (Ident (loc,id),us) as x ->
+ (try CRef (Ident (loc,List.assoc id l),us) with Not_found -> x)
| c -> map_constr_expr_with_binders List.remove_assoc
replace_vars_constr_expr l c
View
4 intf/constrexpr.mli
@@ -62,13 +62,13 @@ and cases_pattern_notation_substitution =
cases_pattern_expr list list (** for recursive notations *)
type constr_expr =
- | CRef of reference
+ | CRef of reference * Univ.universe_list option
| CFix of Loc.t * identifier located * fix_expr list
| CCoFix of Loc.t * identifier located * cofix_expr list
| CProdN of Loc.t * (name located list * binder_kind * constr_expr) list * constr_expr
| CLambdaN of Loc.t * (name located list * binder_kind * constr_expr) list * constr_expr
| CLetIn of Loc.t * name located * constr_expr * constr_expr
- | CAppExpl of Loc.t * (proj_flag * reference) * constr_expr list
+ | CAppExpl of Loc.t * (proj_flag * reference * Univ.universe_list option) * constr_expr list
| CApp of Loc.t * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
| CRecord of Loc.t * constr_expr option * (reference * constr_expr) list
View
2 intf/glob_term.mli
@@ -28,7 +28,7 @@ type cases_pattern =
(** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *)
type glob_constr =
- | GRef of (Loc.t * global_reference)
+ | GRef of (Loc.t * global_reference * Univ.universe_list option)
| GVar of (Loc.t * identifier)
| GEvar of Loc.t * existential_key * glob_constr list option
| GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *)
View
2 kernel/indtypes.ml
@@ -685,6 +685,6 @@ let check_inductive env kn mie =
(* Then check positivity conditions *)
let (nmr,recargs) = check_positivity kn env_ar params inds in
(* Build the inductive packets *)
- build_inductive env mie.mind_entry_polymorphic mie.mind_entry_universes
+ build_inductive env mie.mind_entry_polymorphic (Univ.context_of_universe_context_set univs)
env_ar params mie.mind_entry_record mie.mind_entry_finite
inds nmr recargs
View
11 kernel/inductive.ml
@@ -203,7 +203,16 @@ let fresh_type_of_inductive env (mib, mip) =
(subst_univs_constr subst mip.mind_arity.mind_user_arity,
cst)
-
+let fresh_inductive_instance env ind =
+ let mib, mip = lookup_mind_specif env ind in
+ let inst, ctx = fresh_instance_from mib.mind_universes in
+ ((ind,inst), ctx)
+
+let fresh_constructor_instance env (ind,i) =
+ let mib, mip = lookup_mind_specif env ind in
+ let inst, ctx = fresh_instance_from mib.mind_universes in
+ (((ind,i),inst), ctx)
+
let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args =
type_of_inductive env mip
View
3 kernel/inductive.mli
@@ -42,6 +42,9 @@ val type_of_inductive_knowing_parameters : env -> ?polyprop:bool -> mind_specif
val fresh_type_of_inductive : env -> mind_specif -> types constrained
+val fresh_inductive_instance : env -> inductive -> pinductive in_universe_context_set
+val fresh_constructor_instance : env -> constructor -> pconstructor in_universe_context_set
+
val elim_sorts : mind_specif -> sorts_family list
(** Return type as quoted by the user *)
View
3 kernel/sign.ml
@@ -85,3 +85,6 @@ let push_named_to_rel_context hyps ctxt =
(n+1), (map_rel_declaration (substn_vars n s) d)::ctxt
| [] -> 1, hyps in
snd (subst ctxt)
+
+let subst_univs_context s =
+ map_rel_context (subst_univs_constr s)
View
2 kernel/sign.mli
@@ -62,3 +62,5 @@ val iter_rel_context : (constr -> unit) -> rel_context -> unit
(** {6 Map function of [named_context] } *)
val iter_named_context : (constr -> unit) -> named_context -> unit
+
+val subst_univs_context : Univ.universe_subst -> rel_context -> rel_context
View
12 kernel/term.ml
@@ -1158,22 +1158,26 @@ let strip_lam_n n t = snd (decompose_lam_n n t)
let subst_univs_constr subst c =
if subst = [] then c
else
- let f = List.map (Univ.subst_univs_level subst) in
+ let f = CList.smartmap (Univ.subst_univs_level subst) in
let changed = ref false in
let rec aux t =
match kind_of_term t with
| Const (c, u) ->
let u' = f u in
- if u' = u then t
+ if u' == u then t
else (changed := true; mkConstU (c, u'))
| Ind (i, u) ->
let u' = f u in
- if u' = u then t
+ if u' == u then t
else (changed := true; mkIndU (i, u'))
| Construct (c, u) ->
let u' = f u in
- if u' = u then t
+ if u' == u then t
else (changed := true; mkConstructU (c, u'))
+ | Sort (Type u) ->
+ let u' = subst_univs_universe subst u in
+ if u' == u then t else
+ (changed := true; mkSort (Type u'))
| _ -> map_constr aux t
in
let c' = aux c in
View
4 kernel/typeops.ml
@@ -142,8 +142,8 @@ let fresh_type_of_constant env c =
let fresh_constant_instance env c =
let cb = lookup_constant c env in
- let (univ, subst), cst = fresh_instance_from_context cb.const_universes in
- ((c, univ), cst)
+ let inst, ctx = fresh_instance_from cb.const_universes in
+ ((c, inst), ctx)
let judge_of_constant env cst =
let c = mkConstU cst in
View
2 kernel/typeops.mli
@@ -110,7 +110,7 @@ val type_of_constant_inenv : env -> constant puniverses -> types
val fresh_type_of_constant : env -> constant -> types constrained
val fresh_type_of_constant_body : constant_body -> types constrained
-val fresh_constant_instance : env -> constant -> pconstant constrained
+val fresh_constant_instance : env -> constant -> pconstant in_universe_context_set
val type_of_constant_knowing_parameters : env -> types -> types array -> types
View
13 kernel/univ.ml
@@ -713,6 +713,9 @@ let enforce_eq u v c =
if UniverseLevel.equal u v then c else Constraint.add (u,Eq,v) c
| _ -> anomaly "A universe comparison can only happen between variables"
+let enforce_eq_level u v c =
+ if UniverseLevel.equal u v then c else Constraint.add (u,Eq,v) c
+
let merge_constraints c g =
Constraint.fold enforce_constraint c g
@@ -942,6 +945,16 @@ let fresh_instance_from_context (vars, cst as ctx) =
let constraints = instantiate_univ_context subst ctx in
(inst, subst), constraints
+let fresh_universe_set_instance (ctx, _) =
+ List.fold_left (fun s _ -> UniverseLSet.add (fresh_level ()) s) UniverseLSet.empty ctx
+
+let fresh_instance_from (vars, cst as ctx) =
+ let ctx' = fresh_universe_set_instance ctx in
+ let inst = UniverseLSet.elements ctx' in
+ let subst = List.combine vars inst in
+ let constraints = instantiate_univ_context subst ctx in
+ inst, (ctx', constraints)
+
(* Miscellaneous functions to remove or test local univ assumed to
occur only in the le constraints *)
View
4 kernel/univ.mli
@@ -155,6 +155,9 @@ val instantiate_univ_context : universe_subst -> universe_context -> constraints
val fresh_instance_from_context : universe_context ->
(universe_list * universe_subst) constrained
+val fresh_instance_from : universe_context ->
+ universe_list in_universe_context_set
+
(** Substitution of universes. *)
val subst_univs_level : universe_subst -> universe_level -> universe_level
val subst_univs_universe : universe_subst -> universe -> universe
@@ -167,6 +170,7 @@ type constraint_function = universe -> universe -> constraints -> constraints
val enforce_leq : constraint_function
val enforce_eq : constraint_function
+val enforce_eq_level : universe_level -> universe_level -> constraints -> constraints
(** {6 ... } *)
(** Merge of constraints in a universes graph.
View
4 parsing/egramcoq.ml
@@ -48,7 +48,7 @@ open Egramml
let constr_expr_of_name (loc,na) = match na with
| Anonymous -> CHole (loc,None)
- | Name id -> CRef (Ident (loc,id))
+ | Name id -> CRef (Ident (loc,id),None)
let cases_pattern_expr_of_name (loc,na) = match na with
| Anonymous -> CPatAtom (loc,None)
@@ -77,7 +77,7 @@ let make_constr_action
make (v :: constrs, constrlists, binders) tl)
| ETReference ->
Gram.action (fun (v:reference) ->
- make (CRef v :: constrs, constrlists, binders) tl)
+ make (CRef (v,None) :: constrs, constrlists, binders) tl)
| ETName ->
Gram.action (fun (na:Loc.t * name) ->
make (constr_expr_of_name na :: constrs, constrlists, binders) tl)
View
14 parsing/g_constr.ml4
@@ -159,7 +159,7 @@ GEXTEND Gram
;
constr:
[ [ c = operconstr LEVEL "8" -> c
- | "@"; f=global -> CAppExpl(!@loc,(None,f),[]) ] ]
+ | "@"; f=global -> CAppExpl(!@loc,(None,f,None),[]) ] ]
;
operconstr:
[ "200" RIGHTA
@@ -179,20 +179,20 @@ GEXTEND Gram
| "90" RIGHTA [ ]
| "10" LEFTA
[ f=operconstr; args=LIST1 appl_arg -> CApp(!@loc,(None,f),args)
- | "@"; f=global; args=LIST0 NEXT -> CAppExpl(!@loc,(None,f),args)
+ | "@"; f=global; args=LIST0 NEXT -> CAppExpl(!@loc,(None,f,None),args)
| "@"; (locid,id) = pattern_identref; args=LIST1 identref ->
- let args = List.map (fun x -> CRef (Ident x), None) args in
+ let args = List.map (fun x -> CRef (Ident x,None), None) args in
CApp(!@loc,(None,CPatVar(locid,(true,id))),args) ]
| "9"
[ ".."; c = operconstr LEVEL "0"; ".." ->
- CAppExpl (!@loc,(None,Ident (!@loc,ldots_var)),[c]) ]
+ CAppExpl (!@loc,(None,Ident (!@loc,ldots_var),None),[c]) ]
| "8" [ ]
| "1" LEFTA
[ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
- CApp(!@loc,(Some (List.length args+1),CRef f),args@[c,None])
+ CApp(!@loc,(Some (List.length args+1),CRef (f,None)),args@[c,None])
| c=operconstr; ".("; "@"; f=global;
args=LIST0 (operconstr LEVEL "9"); ")" ->
- CAppExpl(!@loc,(Some (List.length args+1),f),args@[c])
+ CAppExpl(!@loc,(Some (List.length args+1),f,None),args@[c])
| c=operconstr; "%"; key=IDENT -> CDelimiters (!@loc,key,c) ]
| "0"
[ c=atomic_constr -> c
@@ -270,7 +270,7 @@ GEXTEND Gram
| c=operconstr LEVEL "9" -> (c,None) ] ]
;
atomic_constr:
- [ [ g=global -> CRef g
+ [ [ g=global -> CRef (g,None)
| s=sort -> CSort (!@loc,s)
| n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n))
| s=string -> CPrim (!@loc, String s)
View
2 parsing/g_tactic.ml4
@@ -146,7 +146,7 @@ let mkTacCase with_evar = function
(* Reinterpret ident as notations for variables in the context *)
(* because we don't know if they are quantified or not *)
| [ElimOnIdent id,(None,None)],None,None ->
- TacCase (with_evar,(CRef (Ident id),NoBindings))
+ TacCase (with_evar,(CRef (Ident id,None),NoBindings))
| ic ->
if List.exists (function (ElimOnAnonHyp _,_) -> true | _ -> false) (pi1 ic)
then
View
6 parsing/g_xml.ml4
@@ -173,7 +173,7 @@ let rec interp_xml_constr = function
| XmlTag (loc,"META",al,xl) ->
GEvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl))
| XmlTag (loc,"CONST",al,[]) ->
- GRef (loc, ConstRef (get_xml_constant al))
+ GRef (loc, ConstRef (get_xml_constant al), None)
| XmlTag (loc,"MUTCASE",al,x::y::yl) ->
let ind = get_xml_inductive al in
let p = interp_xml_patternsType x in
@@ -186,9 +186,9 @@ let rec interp_xml_constr = function
let nal,rtn = return_type_of_predicate ind n p in
GCases (loc,RegularStyle,rtn,[tm,nal],mat)
| XmlTag (loc,"MUTIND",al,[]) ->
- GRef (loc, IndRef (get_xml_inductive al))
+ GRef (loc, IndRef (get_xml_inductive al), None)
| XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
- GRef (loc, ConstructRef (get_xml_constructor al))
+ GRef (loc, ConstructRef (get_xml_constructor al), None)
| XmlTag (loc,"FIX",al,xl) ->
let li,lnct = List.split (List.map interp_xml_FixFunction xl) in
let ln,lc,lt = List.split3 lnct in
View
4 plugins/decl_mode/decl_interp.ml
@@ -247,7 +247,7 @@ let rec glob_of_pat =
add_params (pred n) (GHole(Loc.ghost,
Evar_kinds.TomatchTypeParameter(ind,n))::q) in
let args = List.map glob_of_pat lpat in
- glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr),
+ glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr,None),
add_params mind.Declarations.mind_nparams args)
let prod_one_hyp = function
@@ -334,7 +334,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
(if expected = 0 then str "none" else int expected) ++ spc () ++
str "expected.") in
let app_ind =
- let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind) in
+ let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind,None) in
let rparams = List.map detype_ground pinfo.per_params in
let rparams_rec =
List.map
View
4 plugins/decl_mode/g_decl_mode.ml4
@@ -191,7 +191,7 @@ GLOBAL: proof_instr;
statement :
[[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c}
| i=ident -> {st_label=Anonymous;
- st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i))}
+ st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i), None)}
| c=constr -> {st_label=Anonymous;st_it=c}
]];
constr_or_thesis :
@@ -204,7 +204,7 @@ GLOBAL: proof_instr;
|
[ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot}
| i=ident -> {st_label=Anonymous;
- st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i)))}
+ st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i), None))}
| c=constr -> {st_label=Anonymous;st_it=This c}
]
];
View
2 pretyping/cases.ml
@@ -1954,7 +1954,7 @@ let vars_of_ctx ctx =
| Some t' when is_topvar t' ->
prev,
(GApp (Loc.ghost,
- (GRef (Loc.ghost, delayed_force coq_eq_refl_ref)),
+ (GRef (Loc.ghost, delayed_force coq_eq_refl_ref, None)),
[hole; GVar (Loc.ghost, prev)])) :: vars
| _ ->
match na with
View
10 pretyping/detyping.ml
@@ -389,7 +389,7 @@ let rec detype (isgoal:bool) avoid env t =
GEvar (dl, n, None)
| Var id ->
(try
- let _ = Global.lookup_named id in GRef (dl, VarRef id)
+ let _ = Global.lookup_named id in GRef (dl, VarRef id,None)
with _ ->
GVar (dl, id))
| Sort s -> GSort (dl,detype_sort s)
@@ -404,14 +404,14 @@ let rec detype (isgoal:bool) avoid env t =
GApp (dl,detype isgoal avoid env f,
Array.map_to_list (detype isgoal avoid env) args)
(* FIXME, should we really forget universes here ? *)
- | Const (sp,u) -> GRef (dl, ConstRef sp)
+ | Const (sp,u) -> GRef (dl, ConstRef sp,Some u)
| Evar (ev,cl) ->
GEvar (dl, ev,
Some (List.map (detype isgoal avoid env) (Array.to_list cl)))
| Ind (ind_sp,u) ->
- GRef (dl, IndRef ind_sp)
+ GRef (dl, IndRef ind_sp,Some u)
| Construct (cstr_sp,u) ->
- GRef (dl, ConstructRef cstr_sp)
+ GRef (dl, ConstructRef cstr_sp,Some u)
| Case (ci,p,c,bl) ->
let comp = computable p (ci.ci_pp_info.ind_nargs) in
detype_case comp (detype isgoal avoid env)
@@ -583,7 +583,7 @@ let rec subst_cases_pattern subst pat =
let rec subst_glob_constr subst raw =
match raw with
- | GRef (loc,ref) ->
+ | GRef (loc,ref,u) ->
let ref',t = subst_global subst ref in
if ref' == ref then raw else
detype false [] [] t
View
24 pretyping/evarconv.ml
@@ -223,9 +223,13 @@ let ise_stack2 no_app env evd f sk1 sk2 =
let exact_ise_stack2 env evd f sk1 sk2 =
match ise_stack2 false env evd f sk1 sk2 with | None, out -> out | _ -> (evd, false)
-let eq_puniverses f (x,u) (y,v) =
- if f x y then try List.for_all2 Univ.eq_levels u v with _ -> false
- else false
+let eq_puniverses evd f (x,u) (y,v) =
+ if f x y then
+ let evdref = ref evd in
+ try List.iter2 (fun x y -> evdref := Evd.set_eq_level !evdref x y) u v;
+ (!evdref, true)
+ with _ -> (evd, false)
+ else (evd, false)
let rec evar_conv_x ts env evd pbty term1 term2 =
let term1 = whd_head_evar evd term1 in
@@ -335,7 +339,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
ise_try evd [f1; f2]
| _, _ ->
- let f1 i =
+ let f1 i = (* FIXME will unfold polymorphic constants always *)
if eq_constr term1 term2 then
exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2
else
@@ -477,14 +481,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
evar_conv_x ts (push_rel (n,None,c) env) i pbty c'1 c'2)]
| Ind sp1, Ind sp2 ->
- if eq_puniverses eq_ind sp1 sp2 then
- exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2
- else (evd, false)
+ ise_and evd
+ [(fun i -> eq_puniverses i eq_ind sp1 sp2);
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
| Construct sp1, Construct sp2 ->
- if eq_puniverses eq_constructor sp1 sp2 then
- exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2
- else (evd, false)
+ ise_and evd
+ [(fun i -> eq_puniverses i eq_constructor sp1 sp2);
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
if Int.equal i1 i2 then
View
19 pretyping/evarutil.ml
@@ -359,6 +359,11 @@ let e_new_evar evdref env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?ca
evdref := evd';
ev
+let e_new_type_evar evdref ?src ?filter env =
+ let evd', e = new_type_evar ?src ?filter !evdref env in
+ evdref := evd';
+ e
+
(*------------------------------------*
* Restricting existing evars *
*------------------------------------*)
@@ -1921,6 +1926,20 @@ let check_evars env initial_sigma sigma c =
| _ -> iter_constr proc_rec c
in proc_rec c
+
+(****************************************)
+(* Operations on universes *)
+(****************************************)
+
+let fresh_constant_instance env evd c =
+ Evd.with_context_set evd (Typeops.fresh_constant_instance env c)
+
+let fresh_inductive_instance env evd i =
+ Evd.with_context_set evd (Inductive.fresh_inductive_instance env i)
+
+let fresh_constructor_instance env evd c =
+ Evd.with_context_set evd (Inductive.fresh_constructor_instance env c)
+
(****************************************)
(* Operations on value/type constraints *)
(****************************************)
View
10 pretyping/evarutil.mli
@@ -42,6 +42,10 @@ val e_new_evar :
val new_type_evar :
?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> evar_map -> env -> evar_map * constr
+val e_new_type_evar : evar_map ref ->
+ ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> env -> constr
+
+
(** Create a fresh evar in a context different from its definition context:
[new_evar_instance sign evd ty inst] creates a new evar of context
[sign] and type [ty], [inst] is a mapping of the evar context to
@@ -143,6 +147,12 @@ val undefined_evars_of_term : evar_map -> constr -> Intset.t
val undefined_evars_of_named_context : evar_map -> named_context -> Intset.t
val undefined_evars_of_evar_info : evar_map -> evar_info -> Intset.t
+(** {6 Universes} *)
+
+val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstant
+val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive
+val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor
+
(** {6 Value/Type constraints} *)
val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment
View
15 pretyping/evd.ml
@@ -209,6 +209,8 @@ module EvarMap = struct
type t = EvarInfoMap.t * universe_context
let empty = EvarInfoMap.empty, empty_universe_context
+ let from_env_and_context e c = EvarInfoMap.empty, (c, universes e)
+
let is_empty (sigma,_) = EvarInfoMap.is_empty sigma
let has_undefined (sigma,_) = EvarInfoMap.has_undefined sigma
let add (sigma,sm) k v = (EvarInfoMap.add sigma k v, sm)
@@ -415,6 +417,9 @@ let empty = {
metas=Metamap.empty
}
+let from_env ?(ctx=Univ.empty_universe_context_set) e =
+ { empty with evars = EvarMap.from_env_and_context e ctx }
+
let has_undefined evd =
EvarMap.has_undefined evd.evars
@@ -506,6 +511,13 @@ let universe_context_set ({evars = (sigma, (ctx, us)) }) = ctx
let universe_context ({evars = (sigma, (ctx, us)) }) =
Univ.context_of_universe_context_set ctx
+let merge_context_set ({evars = (sigma, (ctx, us))} as d) ctx' =
+ {d with evars = (sigma, (Univ.union_universe_context_set ctx ctx',
+ Univ.merge_constraints (snd ctx') us))}
+
+let with_context_set d (a, ctx) =
+ (merge_context_set d ctx, a)
+
let new_univ_variable ({ evars = (sigma, ((vars, cst), us)) } as d) =
let u = Termops.new_univ_level () in
let vars' = Univ.UniverseLSet.add u vars in
@@ -575,6 +587,9 @@ let set_eq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 =
| Type u, Type v when is_univ_var_or_set u && is_univ_var_or_set v ->
add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
| _, _ -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2, []))
+
+let set_eq_level ({evars = (sigma, (us, sm))} as d) u1 u2 =
+ add_constraints d (Univ.enforce_eq_level u1 u2 Univ.empty_constraint)
(**********************************************************)
(* Accessing metas *)
View
8 pretyping/evd.mli
@@ -126,6 +126,8 @@ type evar_map
val progress_evar_map : evar_map -> evar_map -> bool
val empty : evar_map
+val from_env : ?ctx:Univ.universe_context_set -> env -> evar_map
+
val is_empty : evar_map -> bool
(** [has_undefined sigma] is [true] if and only if
there are uninstantiated evars in [sigma]. *)
@@ -244,9 +246,15 @@ val is_sort_variable : evar_map -> sorts -> bool
val whd_sort_variable : evar_map -> constr -> constr
val set_leq_sort : evar_map -> sorts -> sorts -> evar_map
val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
+val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map
val universe_context_set : evar_map -> Univ.universe_context_set
val universe_context : evar_map -> Univ.universe_context
+
+val merge_context_set : evar_map -> Univ.universe_context_set -> evar_map
+
+val with_context_set : evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
+
(********************************************************************
constr with holes *)
type open_constr = evar_map * constr
View
10 pretyping/glob_ops.ml
@@ -227,7 +227,7 @@ let free_glob_vars =
let loc_of_glob_constr = function
- | GRef (loc,_) -> loc
+ | GRef (loc,_,_) -> loc
| GVar (loc,_) -> loc
| GEvar (loc,_,_) -> loc
| GPatVar (loc,_) -> loc
@@ -255,18 +255,18 @@ let rec cases_pattern_of_glob_constr na = function
| Anonymous -> PatVar (loc,Name id)
end
| GHole (loc,_) -> PatVar (loc,na)
- | GRef (loc,ConstructRef cstr) ->
+ | GRef (loc,ConstructRef cstr,_) ->
PatCstr (loc,cstr,[],na)
- | GApp (loc,GRef (_,ConstructRef cstr),l) ->
+ | GApp (loc,GRef (_,ConstructRef cstr,_),l) ->
PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
| _ -> raise Not_found
(* Turn a closed cases pattern into a glob_constr *)
let rec glob_constr_of_closed_cases_pattern_aux = function
| PatCstr (loc,cstr,[],Anonymous) ->
- GRef (loc,ConstructRef cstr)
+ GRef (loc,ConstructRef cstr,None)
| PatCstr (loc,cstr,l,Anonymous) ->
- let ref = GRef (loc,ConstructRef cstr) in
+ let ref = GRef (loc,ConstructRef cstr,None) in
GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l)
| _ -> raise Not_found
View
18 pretyping/indrec.ml
@@ -46,9 +46,9 @@ let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
(* Building case analysis schemes *)
(* Christine Paulin, 1996 *)
-let mis_make_case_com dep env sigma pind (mib,mip as specif) kind =
- let lnamespar = List.map
- (fun (n, c, t) -> (n, c, Termops.refresh_universes t))
+let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
+ let usubst = Univ.make_universe_subst u mib.mind_universes in
+ let lnamespar = Sign.subst_univs_context usubst
mib.mind_params_ctxt
in
@@ -261,13 +261,13 @@ let context_chop k ctx =
| (_, []) -> failwith "context_chop"
in chop_aux [] (k,ctx)
-
(* Main function *)
-let mis_make_indrec env sigma listdepkind mib =
+let mis_make_indrec env sigma listdepkind mib u =
let nparams = mib.mind_nparams in
- let nparrec = mib. mind_nparams_rec in
+ let nparrec = mib.mind_nparams_rec in
+ let usubst = Univ.make_universe_subst u mib.mind_universes in
let lnonparrec,lnamesparrec =
- context_chop (nparams-nparrec) mib.mind_params_ctxt in
+ context_chop (nparams-nparrec) (Sign.subst_univs_context usubst mib.mind_params_ctxt) in
let nrec = List.length listdepkind in
let depPvec =
Array.create mib.mind_ntypes (None : (bool * constr) option) in
@@ -532,12 +532,12 @@ let build_mutual_induction_scheme env sigma = function
lrecspec)
in
let _ = check_arities listdepkind in
- mis_make_indrec env sigma listdepkind mib
+ mis_make_indrec env sigma listdepkind mib u
| _ -> anomaly "build_induction_scheme expects a non empty list of inductive types"
let build_induction_scheme env sigma pind dep kind =
let (mib,mip) = lookup_mind_specif env (fst pind) in
- List.hd (mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib)
+ List.hd (mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind))
(*s Eliminations. *)
View
2 pretyping/patternops.ml
@@ -304,7 +304,7 @@ let rec pat_of_raw metas vars = function
with Not_found -> PVar id)
| GPatVar (_,(false,n)) ->
metas := n::!metas; PMeta (Some n)
- | GRef (_,gr) ->
+ | GRef (_,gr,_) ->
PRef (canonical_gr gr)
(* Hack pour ne pas réécrire une interprétation complète des patterns*)
| GApp (_, GPatVar (_,(true,n)), cl) ->
View
31 pretyping/pretyping.ml
@@ -231,7 +231,22 @@ let evar_kind_of_term sigma c =
(*************************************************************************)
(* Main pretyping function *)
-let pretype_ref loc evdref env = function
+(* Check with universe list? *)
+let pretype_global env evd gr us =
+ match gr with
+ | VarRef id -> evd, mkVar id
+ | ConstRef sp ->
+ let evd, c = with_context_set evd (Typeops.fresh_constant_instance env sp) in
+ evd, mkConstU c
+ | ConstructRef sp ->
+ let evd, c = with_context_set evd (Inductive.fresh_constructor_instance env sp) in
+ evd, mkConstructU c
+ | IndRef sp ->
+ let evd, c = with_context_set evd (Inductive.fresh_inductive_instance env sp) in
+ evd, mkIndU c
+
+let pretype_ref loc evdref env ref us =
+ match ref with
| VarRef id ->
(* Section variable *)
(try let (_,_,ty) = lookup_named id env in make_judge (mkVar id) ty
@@ -241,8 +256,9 @@ let pretype_ref loc evdref env = function
variables *)
Pretype_errors.error_var_not_found_loc loc id)
| ref ->
- let c = constr_of_global ref in
- make_judge c (Retyping.get_type_of env Evd.empty c)
+ let evd, c = pretype_global env !evdref ref us in
+ evdref := evd;
+ make_judge c (Retyping.get_type_of env evd c)
let pretype_sort evdref = function
| GProp -> judge_of_prop
@@ -256,9 +272,9 @@ let new_type_evar evdref env loc =
(* in environment [env], with existential variables [evdref] and *)
(* the type constraint tycon *)
let rec pretype (tycon : type_constraint) env evdref lvar = function
- | GRef (loc,ref) ->
+ | GRef (loc,ref,us) ->
inh_conv_coerce_to_tycon loc env evdref
- (pretype_ref loc evdref env ref)
+ (pretype_ref loc evdref env ref us)
tycon
| GVar (loc, id) ->
@@ -706,11 +722,6 @@ let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
if fail_evar then check_evars env Evd.empty !evdref c;
c
-(* TODO: comment faire remonter l'information si le typage a resolu des
- variables du sigma original. il faudrait que la fonction de typage
- retourne aussi le nouveau sigma...
-*)
-
let understand_judgment sigma env c =
let evdref = ref sigma in
let j = pretype empty_tycon env evdref ([],[]) c in
View
22 printing/ppconstr.ml
@@ -119,6 +119,12 @@ let pr_name = pr_name
let pr_qualid = pr_qualid
let pr_patvar = pr_id
+let pr_universe_list l =
+ pr_opt (pr_in_comment Univ.pr_universe_list) l
+
+let pr_cref ref us =
+ pr_reference ref ++ pr_universe_list us
+
let pr_expl_args pr (a,expl) =
match expl with
| None -> pr (lapp,L) a
@@ -397,7 +403,7 @@ let pr_simple_return_type pr na po =
let pr_proj pr pr_app a f l =
hov 0 (pr (lproj,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
-let pr_appexpl pr f l =
+let pr_appexpl pr (f,us) l =
hov 2 (
str "@" ++ pr_reference f ++
prlist (pr_sep_com spc (pr (lapp,L))) l)
@@ -421,7 +427,7 @@ let pr_dangling_with_for sep pr inherited a =
let pr pr sep inherited a =
let (strm,prec) = match a with
- | CRef r -> pr_reference r, latom
+ | CRef (r,us) -> pr_cref r us, latom
| CFix (_,id,fix) ->
hov 0 (str"fix " ++
pr_recursive
@@ -458,19 +464,19 @@ let pr pr sep inherited a =
pr spc ltop a ++ str " in") ++
pr spc ltop b),
lletin
- | CAppExpl (_,(Some i,f),l) ->
+ | CAppExpl (_,(Some i,f,us),l) ->
let l1,l2 = List.chop i l in
let c,l1 = List.sep_last l1 in
- let p = pr_proj (pr mt) pr_appexpl c f l1 in
+ let p = pr_proj (pr mt) pr_appexpl c (f,us) l1 in
if l2<>[] then
p ++ prlist (pr spc (lapp,L)) l2, lapp
else
p, lproj
- | CAppExpl (_,(None,Ident (_,var)),[t])
- | CApp (_,(_,CRef(Ident(_,var))),[t,None])
+ | CAppExpl (_,(None,Ident (_,var),us),[t])
+ | CApp (_,(_,CRef(Ident(_,var),us)),[t,None])
when var = Notation_ops.ldots_var ->
hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg
- | CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp
+ | CAppExpl (_,(None,f,us),l) -> pr_appexpl (pr mt) (f,us) l, lapp
| CApp (_,(Some i,f),l) ->
let l1,l2 = List.chop i l in
let c,l1 = List.sep_last l1 in
@@ -566,7 +572,7 @@ let rec fix rf x =rf (fix rf) x
let pr = fix modular_constr_pr mt
let pr_simpleconstr = function
- | CAppExpl (_,(None,f),[]) -> str "@" ++ pr_reference f
+ | CAppExpl (_,(None,f,us),[]) -> str "@" ++ pr_cref f us
| c -> pr lsimpleconstr c
let default_term_pr = {
View
6 proofs/pfedit.ml
@@ -145,7 +145,8 @@ open Decl_kinds
let next = let n = ref 0 in fun () -> incr n; !n
let build_constant_by_tactic id sign typ tac =
- start_proof id (Global,false,Proof Theorem) sign typ (fun _ _ -> ());
+ start_proof id (Global,false(*FIXME*),Proof Theorem) sign
+ typ (fun _ _ -> ());
try
by tac;
let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
@@ -175,6 +176,7 @@ let solve_by_implicit_tactic env sigma (evk,args) =
when
Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
(Environ.named_context env) ->
- (try build_by_tactic env evi.evar_concl (tclCOMPLETE tac)
+ (try build_by_tactic env (evi.evar_concl, Evd.universe_context_set sigma)
+ (tclCOMPLETE tac)
with e when Logic.catchable_exception e -> raise Exit)
| _ -> raise Exit
View
7 proofs/pfedit.mli
@@ -75,7 +75,7 @@ val current_proof_depth: unit -> int
type lemma_possible_guards = Proof_global.lemma_possible_guards
val start_proof :
- identifier -> goal_kind -> named_context_val -> constr ->
+ identifier -> goal_kind -> named_context_val -> constr Univ.in_universe_context_set ->
?init_tac:tactic -> ?compute_guard:lemma_possible_guards ->
unit declaration_hook -> unit
@@ -165,9 +165,10 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
(** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
-val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic ->
+val build_constant_by_tactic : identifier -> named_context_val ->
+ types Univ.in_universe_context_set -> tactic ->
Entries.definition_entry
-val build_by_tactic : env -> types -> tactic -> constr
+val build_by_tactic : env -> types Univ.in_universe_context_set -> tactic -> constr
(** Declare the default tactic to fill implicit arguments *)
View
4 proofs/proof.ml
@@ -178,7 +178,7 @@ let has_unresolved_evar p =
(* Returns the list of partial proofs to initial goals *)
let partial_proof p =
- List.map fst (Proofview.return p.state.proofview)
+ List.map fst (fst (Proofview.return p.state.proofview)) (*FIXME: unsafe?*)
@@ -383,7 +383,7 @@ let start goals =
undo_stack = [] ;
transactions = [] ;
info = { endline_tactic = Proofview.tclUNIT ();
- initial_conclusions = List.map snd goals;
+ initial_conclusions = List.map (fun x -> fst (snd x)) goals;
section_vars = None }
}
in
View
4 proofs/proof.mli
@@ -46,7 +46,7 @@ val proof : proof -> Goal.goal list * (Goal.goal list * Goal.goal list) list * E
(*** General proof functions ***)
-val start : (Environ.env * Term.types) list -> proof
+val start : (Environ.env * Term.types Univ.in_universe_context_set) list -> proof
(* Returns [true] if the considered proof is completed, that is if no goal remain
to be considered (this does not require that all evars have been solved). *)
@@ -60,7 +60,7 @@ val partial_proof : proof -> Term.constr list
Raises [HasUnresolvedEvar] if some evars have been left undefined. *)
exception UnfinishedProof
exception HasUnresolvedEvar
-val return : proof -> (Term.constr * Term.types) list
+val return : proof -> (Term.constr * Term.types) list Univ.in_universe_context
(* Interpretes the Undo command. Raises [EmptyUndoStack] if
the undo stack is empty. *)
View
13 proofs/proof_global.ml
@@ -264,21 +264,20 @@ let close_proof () =
try
let id = get_current_proof_name () in
let p = give_me_the_proof () in
- let proofs_and_types = Proof.return p in
+ let proofs_and_types, ctx = Proof.return p in
let section_vars = Proof.get_used_variables p in
+ let { compute_guard=cg ; strength=str ; hook=hook } =
+ Idmap.find id !proof_info
+ in
let entries = List.map
(fun (c,t) -> { Entries.const_entry_body = c;
const_entry_secctx = section_vars;
const_entry_type = Some t;
- (* FIXME *)
- const_entry_polymorphic = false;
- const_entry_universes = Univ.empty_universe_context;
+ const_entry_polymorphic = Util.pi2 str;
+ const_entry_universes = ctx;
const_entry_opaque = true })
proofs_and_types
in
- let { compute_guard=cg ; strength=str ; hook=hook } =
- Idmap.find id !proof_info
- in
(id, (entries,cg,str,hook))
with
| Proof.UnfinishedProof ->
View
2 proofs/proof_global.mli
@@ -55,7 +55,7 @@ val give_me_the_proof : unit -> Proof.proof
type lemma_possible_guards = int list list
val start_proof : Names.identifier ->
Decl_kinds.goal_kind ->
- (Environ.env * Term.types) list ->
+ (Environ.env * Term.types Univ.in_universe_context_set) list ->
?compute_guard:lemma_possible_guards ->
unit Tacexpr.declaration_hook ->
unit
View
6 proofs/proofview.ml
@@ -40,13 +40,14 @@ let init =
solution = Evd.empty ;
comb = []
}
- | (env,typ)::l -> let { initial = ret ; solution = sol ; comb = comb } =
+ | (env,(typ,ctx))::l -> let { initial = ret ; solution = sol ; comb = comb } =
aux l
in
let ( new_defs , econstr ) =
Evarutil.new_evar sol env typ
in
let (e,_) = Term.destEvar econstr in
+ let new_defs = Evd.merge_context_set new_defs ctx in
let gl = Goal.build e in
{ initial = (econstr,typ)::ret;
solution = new_defs ;
@@ -65,7 +66,8 @@ let finished = function
(* Returns the current value of the proofview partial proofs. *)
let return { initial=init; solution=defs } =
- List.map (fun (c,t) -> (Evarutil.nf_evar defs c , t)) init
+ (List.map (fun (c,t) -> (Evarutil.nf_evar defs c , t)) init,
+ Evd.universe_context defs)
(* spiwack: this function should probably go in the Util section,
but I'd rather have Util (or a separate module for lists)
View
4 proofs/proofview.mli
@@ -36,15 +36,15 @@ val proofview : proofview -> Goal.goal list * Evd.evar_map
(* Initialises a proofview, the argument is a list of environement,
conclusion types, creating that many initial goals. *)
-val init : (Environ.env * Term.types) list -> proofview
+val init : (Environ.env * Term.types Univ.in_universe_context_set) list -> proofview
(* Returns whether this proofview is finished or not.That is,
if it has empty subgoals in the comb. There could still be unsolved
subgoaled, but they would then be out of the view, focused out. *)
val finished : proofview -> bool
(* Returns the current value of the proofview partial proofs. *)
-val return : proofview -> (constr*types) list
+val return : proofview -> (constr*types) list Univ.in_universe_context
(*** Focusing operations ***)
View
14 tactics/elimschemes.ml
@@ -40,12 +40,17 @@ let optimize_non_type_induction_scheme kind dep sort ind =
mib.mind_nparams_rec
else
mib.mind_nparams in
- snd (weaken_sort_scheme (new_sort_in_family sort) npars c t)
+ (snd (weaken_sort_scheme (new_sort_in_family sort) npars c t),
+ Univ.empty_universe_context) (* FIXME *)
else
- build_induction_scheme (Global.env()) Evd.empty (ind,[]) dep sort
+ let env = Global.env () in
+ let sigma, indu = Evarutil.fresh_inductive_instance env (Evd.from_env env) ind in
+ build_induction_scheme env sigma indu dep sort, Evd.universe_context sigma
let build_induction_scheme_in_type dep sort ind =
- build_induction_scheme (Global.env()) Evd.empty (ind,[]) dep sort
+ let env = Global.env () in
+ let sigma, indu = Evarutil.fresh_inductive_instance env (Evd.from_env env) ind in
+ build_induction_scheme env sigma indu dep sort, Evd.universe_context sigma