1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 exception Impossible of int;;
29 exception NotWellTyped of string;;
30 exception WrongUriToConstant of string;;
31 exception WrongUriToVariable of string;;
32 exception WrongUriToMutualInductiveDefinitions of string;;
33 exception ListTooShort;;
34 exception RelToHiddenHypothesis;;
36 let syntactic_equality_add_time = ref 0.0;;
37 let type_of_aux'_add_time = ref 0.0;;
38 let number_new_type_of_aux'_double_work = ref 0;;
39 let number_new_type_of_aux' = ref 0;;
40 let number_new_type_of_aux'_prop = ref 0;;
42 let double_work = ref 0;;
44 let xxx_type_of_aux' m c t =
45 let t1 = Sys.time () in
46 let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in
47 let t2 = Sys.time () in
48 type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
52 type types = {synthesized : Cic.term ; expected : Cic.term option};;
54 (* does_not_occur n te *)
55 (* returns [true] if [Rel n] does not occur in [te] *)
56 let rec does_not_occur n =
59 C.Rel m when m = n -> false
63 | C.Implicit _ -> true
65 does_not_occur n te && does_not_occur n ty
66 | C.Prod (name,so,dest) ->
67 does_not_occur n so &&
68 does_not_occur (n + 1) dest
69 | C.Lambda (name,so,dest) ->
70 does_not_occur n so &&
71 does_not_occur (n + 1) dest
72 | C.LetIn (name,so,dest) ->
73 does_not_occur n so &&
74 does_not_occur (n + 1) dest
76 List.fold_right (fun x i -> i && does_not_occur n x) l true
77 | C.Var (_,exp_named_subst)
78 | C.Const (_,exp_named_subst)
79 | C.MutInd (_,_,exp_named_subst)
80 | C.MutConstruct (_,_,_,exp_named_subst) ->
81 List.fold_right (fun (_,x) i -> i && does_not_occur n x)
83 | C.MutCase (_,_,out,te,pl) ->
84 does_not_occur n out && does_not_occur n te &&
85 List.fold_right (fun x i -> i && does_not_occur n x) pl true
87 let len = List.length fl in
88 let n_plus_len = n + len in
90 List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
94 i && does_not_occur n ty &&
95 does_not_occur n_plus_len bo
98 let len = List.length fl in
99 let n_plus_len = n + len in
101 List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
105 i && does_not_occur n ty &&
106 does_not_occur n_plus_len bo
110 let rec beta_reduce =
111 let module S = CicSubstitution in
112 let module C = Cic in
115 | C.Var (uri,exp_named_subst) ->
116 let exp_named_subst' =
117 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
119 C.Var (uri,exp_named_subst')
123 (function None -> None | Some t -> Some (beta_reduce t)) l
126 | C.Implicit _ -> assert false
128 C.Cast (beta_reduce te, beta_reduce ty)
130 C.Prod (n, beta_reduce s, beta_reduce t)
131 | C.Lambda (n,s,t) ->
132 C.Lambda (n, beta_reduce s, beta_reduce t)
134 C.LetIn (n, beta_reduce s, beta_reduce t)
135 | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
136 let he' = S.subst he t in
141 C.Appl l -> beta_reduce (C.Appl (l@tl))
142 | _ -> beta_reduce (C.Appl (he'::tl)))
144 C.Appl (List.map beta_reduce l)
145 | C.Const (uri,exp_named_subst) ->
146 let exp_named_subst' =
147 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
149 C.Const (uri,exp_named_subst')
150 | C.MutInd (uri,i,exp_named_subst) ->
151 let exp_named_subst' =
152 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
154 C.MutInd (uri,i,exp_named_subst')
155 | C.MutConstruct (uri,i,j,exp_named_subst) ->
156 let exp_named_subst' =
157 List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
159 C.MutConstruct (uri,i,j,exp_named_subst')
160 | C.MutCase (sp,i,outt,t,pl) ->
161 C.MutCase (sp,i,beta_reduce outt,beta_reduce t,
162 List.map beta_reduce pl)
166 (function (name,i,ty,bo) ->
167 name,i,beta_reduce ty,beta_reduce bo
174 (function (name,ty,bo) ->
175 name,beta_reduce ty,beta_reduce bo
181 (* syntactic_equality up to the *)
182 (* distinction between fake dependent products *)
183 (* and non-dependent products, alfa-conversion *)
184 (*CSC: must alfa-conversion be considered or not? *)
185 let syntactic_equality t t' =
186 let module C = Cic in
187 let rec syntactic_equality t t' =
191 C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') ->
192 UriManager.eq uri uri' &&
193 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
194 | C.Cast (te,ty), C.Cast (te',ty') ->
195 syntactic_equality te te' &&
196 syntactic_equality ty ty'
197 | C.Prod (_,s,t), C.Prod (_,s',t') ->
198 syntactic_equality s s' &&
199 syntactic_equality t t'
200 | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
201 syntactic_equality s s' &&
202 syntactic_equality t t'
203 | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
204 syntactic_equality s s' &&
205 syntactic_equality t t'
206 | C.Appl l, C.Appl l' ->
207 List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
208 | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') ->
209 UriManager.eq uri uri' &&
210 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
211 | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') ->
212 UriManager.eq uri uri' && i = i' &&
213 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
214 | C.MutConstruct (uri,i,j,exp_named_subst),
215 C.MutConstruct (uri',i',j',exp_named_subst') ->
216 UriManager.eq uri uri' && i = i' && j = j' &&
217 syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
218 | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
219 UriManager.eq sp sp' && i = i' &&
220 syntactic_equality outt outt' &&
221 syntactic_equality t t' &&
223 (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
224 | C.Fix (i,fl), C.Fix (i',fl') ->
227 (fun b (_,i,ty,bo) (_,i',ty',bo') ->
229 syntactic_equality ty ty' &&
230 syntactic_equality bo bo') true fl fl'
231 | C.CoFix (i,fl), C.CoFix (i',fl') ->
234 (fun b (_,ty,bo) (_,ty',bo') ->
236 syntactic_equality ty ty' &&
237 syntactic_equality bo bo') true fl fl'
238 | _, _ -> false (* we already know that t != t' *)
239 and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 =
241 (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true
242 exp_named_subst1 exp_named_subst2
245 syntactic_equality t t'
250 let xxx_syntactic_equality t t' =
251 let t1 = Sys.time () in
252 let res = syntactic_equality t t' in
253 let t2 = Sys.time () in
254 syntactic_equality_add_time := !syntactic_equality_add_time +. t2 -. t1 ;
262 | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
263 | (_,_) -> raise ListTooShort
266 let type_of_constant uri =
267 let module C = Cic in
268 let module R = CicReduction in
269 let module U = UriManager in
271 match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
272 CicEnvironment.CheckedObj (cobj,_) -> cobj
273 | CicEnvironment.UncheckedObj uobj ->
274 raise (NotWellTyped "Reference to an unchecked constant")
277 C.Constant (_,_,ty,_,_) -> ty
278 | C.CurrentProof (_,_,_,ty,_,_) -> ty
279 | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
282 let type_of_variable uri =
283 let module C = Cic in
284 let module R = CicReduction in
285 let module U = UriManager in
286 match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
287 CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
288 | CicEnvironment.UncheckedObj (C.Variable _) ->
289 raise (NotWellTyped "Reference to an unchecked variable")
290 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
293 let type_of_mutual_inductive_defs uri i =
294 let module C = Cic in
295 let module R = CicReduction in
296 let module U = UriManager in
298 match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
299 CicEnvironment.CheckedObj (cobj,_) -> cobj
300 | CicEnvironment.UncheckedObj uobj ->
301 raise (NotWellTyped "Reference to an unchecked inductive type")
304 C.InductiveDefinition (dl,_,_,_) ->
305 let (_,_,arity,_) = List.nth dl i in
307 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
310 let type_of_mutual_inductive_constr uri i j =
311 let module C = Cic in
312 let module R = CicReduction in
313 let module U = UriManager in
315 match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
316 CicEnvironment.CheckedObj (cobj,_) -> cobj
317 | CicEnvironment.UncheckedObj uobj ->
318 raise (NotWellTyped "Reference to an unchecked constructor")
321 C.InductiveDefinition (dl,_,_,_) ->
322 let (_,_,_,cl) = List.nth dl i in
323 let (_,ty) = List.nth cl (j-1) in
325 | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
328 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
329 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
330 (* Coscoy's double type-inference algorithm *)
331 (* It computes the inner-types of every subterm of [t], *)
332 (* even when they are not needed to compute the types *)
333 (* of other terms. *)
334 let rec type_of_aux context t expectedty =
335 let module C = Cic in
336 let module R = CicReduction in
337 let module S = CicSubstitution in
338 let module U = UriManager in
343 match List.nth context (n - 1) with
344 Some (_,C.Decl t) -> S.lift n t
345 | Some (_,C.Def (_,Some ty)) -> S.lift n ty
346 | Some (_,C.Def (bo,None)) ->
347 type_of_aux context (S.lift n bo) expectedty
348 | None -> raise RelToHiddenHypothesis
350 _ -> raise (NotWellTyped "Not a close term")
352 | C.Var (uri,exp_named_subst) ->
353 visit_exp_named_subst context uri exp_named_subst ;
354 CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
356 (* Let's visit all the subterms that will not be visited later *)
357 let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
358 let lifted_canonical_context =
362 | (Some (n,C.Decl t))::tl ->
363 (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
364 | (Some (n,C.Def (t,None)))::tl ->
365 (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::
367 | None::tl -> None::(aux (i+1) tl)
368 | (Some (_,C.Def (_,Some _)))::_ -> assert false
370 aux 1 canonical_context
377 | Some t,Some (_,C.Def (ct,_)) ->
380 (xxx_type_of_aux' metasenv context ct)
382 (* Maybe I am a bit too paranoid, because *)
383 (* if the term is well-typed than t and ct *)
384 (* are convertible. Nevertheless, I compute *)
385 (* the expected type. *)
386 ignore (type_of_aux context t (Some expected_type))
387 | Some t,Some (_,C.Decl ct) ->
388 ignore (type_of_aux context t (Some ct))
389 | _,_ -> assert false (* the term is not well typed!!! *)
390 ) l lifted_canonical_context
392 let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
393 (* Checks suppressed *)
394 CicSubstitution.subst_meta l ty
395 | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
396 C.Sort (C.Type (CicUniv.fresh()))
397 | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *)
398 | C.Implicit _ -> raise (Impossible 21)
400 (* Let's visit all the subterms that will not be visited later *)
401 let _ = type_of_aux context te (Some (beta_reduce ty)) in
402 let _ = type_of_aux context ty None in
403 (* Checks suppressed *)
405 | C.Prod (name,s,t) ->
406 let sort1 = type_of_aux context s None
407 and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
408 sort_of_prod context (name,s) (sort1,sort2)
409 | C.Lambda (n,s,t) ->
410 (* Let's visit all the subterms that will not be visited later *)
411 let _ = type_of_aux context s None in
412 let expected_target_type =
413 match expectedty with
415 | Some expectedty' ->
417 match R.whd context expectedty' with
418 C.Prod (_,_,expected_target_type) ->
419 beta_reduce expected_target_type
425 type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
427 (* Checks suppressed *)
430 (*CSC: What are the right expected types for the source and *)
431 (*CSC: target of a LetIn? None used. *)
432 (* Let's visit all the subterms that will not be visited later *)
433 let ty = type_of_aux context s None in
435 (* Checks suppressed *)
436 type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None
437 in (* CicSubstitution.subst s t_typ *)
438 if does_not_occur 1 t_typ then
439 (* since [Rel 1] does not occur in typ, substituting any term *)
440 (* in place of [Rel 1] is equivalent to delifting once *)
441 CicSubstitution.subst (C.Implicit None) t_typ
444 | C.Appl (he::tl) when List.length tl > 0 ->
446 let expected_hetype =
447 (* Inefficient, the head is computed twice. But I know *)
448 (* of no other solution. *)
450 (R.whd context (xxx_type_of_aux' metasenv context he)))
452 let hetype = type_of_aux context he (Some expected_hetype) in
453 let tlbody_and_type =
457 | C.Prod (n,s,t),he::tl ->
458 (he, type_of_aux context he (Some (beta_reduce s)))::
459 (aux (R.whd context (S.subst he t), tl))
462 aux (expected_hetype, tl) *)
463 let hetype = R.whd context (type_of_aux context he None) in
464 let tlbody_and_type =
468 | C.Prod (n,s,t),he::tl ->
469 (he, type_of_aux context he (Some (beta_reduce s)))::
470 (aux (R.whd context (S.subst he t), tl))
475 eat_prods context hetype tlbody_and_type
476 | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
477 | C.Const (uri,exp_named_subst) ->
478 visit_exp_named_subst context uri exp_named_subst ;
479 CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
480 | C.MutInd (uri,i,exp_named_subst) ->
481 visit_exp_named_subst context uri exp_named_subst ;
482 CicSubstitution.subst_vars exp_named_subst
483 (type_of_mutual_inductive_defs uri i)
484 | C.MutConstruct (uri,i,j,exp_named_subst) ->
485 visit_exp_named_subst context uri exp_named_subst ;
486 CicSubstitution.subst_vars exp_named_subst
487 (type_of_mutual_inductive_constr uri i j)
488 | C.MutCase (uri,i,outtype,term,pl) ->
489 let outsort = type_of_aux context outtype None in
490 let (need_dummy, k) =
491 let rec guess_args context t =
492 match CicReduction.whd context t with
493 C.Sort _ -> (true, 0)
494 | C.Prod (name, s, t) ->
495 let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
497 (* last prod before sort *)
498 match CicReduction.whd context s with
499 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
501 | C.Appl ((C.MutInd (uri',i',_)) :: _)
502 when U.eq uri' uri && i' = i -> (false, 1)
506 | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
508 let (b, k) = guess_args context outsort in
509 if not b then (b, k - 1) else (b, k)
511 let (parameters, arguments,exp_named_subst) =
513 xxx_type_of_aux' metasenv context term
516 R.whd context (type_of_aux context term
517 (Some (beta_reduce type_of_term)))
519 (*CSC manca il caso dei CAST *)
520 C.MutInd (uri',i',exp_named_subst) ->
521 (* Checks suppressed *)
522 [],[],exp_named_subst
523 | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
525 split tl (List.length tl - k)
526 in params,args,exp_named_subst
528 raise (NotWellTyped "MutCase: the term is not an inductive one")
530 (* Checks suppressed *)
531 (* Let's visit all the subterms that will not be visited later *)
535 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
536 with Not_found -> assert false
539 C.InductiveDefinition (tl,_,parsno,_) ->
540 let (_,_,_,cl) = List.nth tl i in (cl,parsno)
542 raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
548 if parameters = [] then
549 (C.MutConstruct (uri,i,j,exp_named_subst))
551 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
554 type_of_branch context parsno need_dummy outtype cons
555 (xxx_type_of_aux' metasenv context cons)
557 ignore (type_of_aux context p
558 (Some (beta_reduce expectedtype))) ;
560 ) 1 (List.combine pl cl)
562 if not need_dummy then
563 C.Appl ((outtype::arguments)@[term])
564 else if arguments = [] then
567 C.Appl (outtype::arguments)
569 (* Let's visit all the subterms that will not be visited later *)
574 let _ = type_of_aux context ty None in
575 (Some (C.Name n,(C.Decl ty)))
584 beta_reduce (CicSubstitution.lift (List.length fl) ty)
586 ignore (type_of_aux context' bo (Some expectedty))
589 (* Checks suppressed *)
590 let (_,_,ty,_) = List.nth fl i in
593 (* Let's visit all the subterms that will not be visited later *)
598 let _ = type_of_aux context ty None in
599 (Some (C.Name n,(C.Decl ty)))
608 beta_reduce (CicSubstitution.lift (List.length fl) ty)
610 ignore (type_of_aux context' bo (Some expectedty))
613 (* Checks suppressed *)
614 let (_,ty,_) = List.nth fl i in
617 let synthesized' = beta_reduce synthesized in
619 match expectedty with
621 (* No expected type *)
622 {synthesized = synthesized' ; expected = None}, synthesized
623 | Some ty when xxx_syntactic_equality synthesized' ty ->
624 (* The expected type is synthactically equal to *)
625 (* the synthesized type. Let's forget it. *)
626 {synthesized = synthesized' ; expected = None}, synthesized
627 | Some expectedty' ->
628 {synthesized = synthesized' ; expected = Some expectedty'},
631 assert (not (Cic.CicHash.mem subterms_to_types t));
632 Cic.CicHash.add subterms_to_types t types ;
635 and visit_exp_named_subst context uri exp_named_subst =
639 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
640 with Not_found -> assert false
642 let params = CicUtil.params_of_obj obj in
647 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
648 with Not_found -> assert false
651 Cic.Variable (_,None,ty,_,_) -> uri,ty
652 | _ -> assert false (* the theorem is well-typed *)
655 let rec check uris_and_types subst =
656 match uris_and_types,subst with
658 | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
659 ignore (type_of_aux context t (Some ty)) ;
662 (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
665 | _,_ -> assert false (* the theorem is well-typed *)
667 check uris_and_types exp_named_subst
669 and sort_of_prod context (name,s) (t1, t2) =
670 let module C = Cic in
671 let t1' = CicReduction.whd context t1 in
672 let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
673 match (t1', t2') with
674 (C.Sort _, C.Sort s2)
675 when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
676 (* different from Coq manual!!! *)
678 | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
679 C.Sort (C.Type (CicUniv.fresh()))
680 | (C.Sort _,C.Sort (C.Type t1)) ->
681 (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
682 C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
683 | (C.Meta _, C.Sort _) -> t2'
684 | (C.Meta _, (C.Meta (_,_) as t))
685 | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
690 ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
692 and eat_prods context hetype =
693 (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
697 | (hete, hety)::tl ->
698 (match (CicReduction.whd context hetype) with
700 (* Checks suppressed *)
701 eat_prods context (CicSubstitution.subst hete t) tl
702 | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
705 and type_of_branch context argsno need_dummy outtype term constype =
706 let module C = Cic in
707 let module R = CicReduction in
708 match R.whd context constype with
713 C.Appl [outtype ; term]
714 | C.Appl (C.MutInd (_,_,_)::tl) ->
715 let (_,arguments) = split tl argsno
717 if need_dummy && arguments = [] then
720 C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
721 | C.Prod (name,so,de) ->
723 match CicSubstitution.lift 1 term with
724 C.Appl l -> C.Appl (l@[C.Rel 1])
725 | t -> C.Appl [t ; C.Rel 1]
727 C.Prod (C.Anonymous,so,type_of_branch
728 ((Some (name,(C.Decl so)))::context) argsno need_dummy
729 (CicSubstitution.lift 1 outtype) term' de)
730 | _ -> raise (Impossible 20)
733 type_of_aux context t expectedty
736 let double_type_of metasenv context t expectedty =
737 let subterms_to_types = Cic.CicHash.create 503 in
738 ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;