summaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_pretyping_F.ml
blob: 7fcd426769b78408cd7a8a4262285cc36ca40612 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id: subtac_pretyping_F.ml 13332 2010-07-26 22:12:43Z msozeau $ *)

open Pp
open Util
open Names
open Sign
open Evd
open Term
open Termops
open Reductionops
open Environ
open Type_errors
open Typeops
open Libnames
open Nameops
open Classops
open List
open Recordops
open Evarutil
open Pretype_errors
open Rawterm
open Evarconv
open Pattern
open Pretyping

(************************************************************************)
(* This concerns Cases *)
open Declarations
open Inductive
open Inductiveops

module SubtacPretyping_F (Coercion : Coercion.S) = struct

  module Cases = Subtac_cases.Cases_F(Coercion)

  (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
  let allow_anonymous_refs = ref true

  let evd_comb0 f evdref =
    let (evd',x) = f !evdref in
      evdref := evd';
      x

  let evd_comb1 f evdref x =
    let (evd',y) = f !evdref x in
      evdref := evd';
      y

  let evd_comb2 f evdref x y =
    let (evd',z) = f !evdref x y in
      evdref := evd';
      z

  let evd_comb3 f evdref x y z =
    let (evd',t) = f !evdref x y z in
      evdref := evd';
      t

  let mt_evd = Evd.empty

  (* Utilisé pour inférer le prédicat des Cases *)
  (* Semble exagérement fort *)
  (* Faudra préférer une unification entre les types de toutes les clauses *)
  (* et autoriser des ? à rester dans le résultat de l'unification *)

  let evar_type_fixpoint loc env evdref lna lar vdefj =
    let lt = Array.length vdefj in
      if Array.length lar = lt then
	for i = 0 to lt-1 do
          if not (e_cumul env evdref (vdefj.(i)).uj_type
		    (lift lt lar.(i))) then
            error_ill_typed_rec_body_loc loc env ( !evdref)
              i lna vdefj lar
	done

  let check_branches_message loc env evdref c (explft,lft) =
    for i = 0 to Array.length explft - 1 do
      if not (e_cumul env evdref lft.(i) explft.(i)) then
	let sigma =  !evdref in
	  error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
    done

  (* coerce to tycon if any *)
  let inh_conv_coerce_to_tycon loc env evdref j = function
    | None -> j_nf_evar !evdref j
    | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t

  let push_rels vars env = List.fold_right push_rel vars env

  (*
    let evar_type_case evdref env ct pt lft p c =
    let (mind,bty,rslty) = type_case_branches env ( evdref) ct pt p c
    in check_branches_message evdref env (c,ct) (bty,lft); (mind,rslty)
  *)

  let strip_meta id = (* For Grammar v7 compatibility *)
    let s = string_of_id id in
      if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
      else id

  let invert_ltac_bound_name env id0 id =
    try mkRel (pi1 (lookup_rel_id id (rel_context env)))
    with Not_found ->
      errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
	str " depends on pattern variable name " ++ pr_id id ++
	str " which is not bound in current context")

  let pretype_id loc env sigma (lvar,unbndltacvars) id =
    let id = strip_meta id in (* May happen in tactics defined by Grammar *)
      try
	let (n,_,typ) = lookup_rel_id id (rel_context env) in
	  { uj_val  = mkRel n; uj_type = lift n typ }
      with Not_found ->
	try
	  let (ids,c) = List.assoc id lvar in
	  let subst = List.map (invert_ltac_bound_name env id) ids in
	  let c = substl subst c in
	  { uj_val = c; uj_type = Retyping.get_type_of env sigma c }
	with Not_found ->
	  try
	    let (_,_,typ) = lookup_named id env in
	      { uj_val  = mkVar id; uj_type = typ }
	  with Not_found ->
	    try (* To build a nicer ltac error message *)
	      match List.assoc id unbndltacvars with
		| None -> user_err_loc (loc,"",
					str "variable " ++ pr_id id ++ str " should be bound to a term")
		| Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
	    with Not_found ->
	      error_var_not_found_loc loc id

  (* make a dependent predicate from an undependent one *)

  let make_dep_of_undep env (IndType (indf,realargs)) pj =
    let n = List.length realargs in
    let rec decomp n p =
      if n=0 then p else
	match kind_of_term p with
	  | Lambda (_,_,c) -> decomp (n-1) c
	  | _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1]))
    in
    let sign,s = decompose_prod_n n pj.uj_type in
    let ind = build_dependent_inductive env indf in
    let s' = mkProd (Anonymous, ind, s) in
    let ccl = lift 1 (decomp n pj.uj_val) in
    let ccl' = mkLambda (Anonymous, ind, ccl) in
      {uj_val=it_mkLambda ccl' sign; uj_type=it_mkProd s' sign}

  (*************************************************************************)
  (* Main pretyping function                                               *)

  let pretype_ref evdref env ref =
    let c = constr_of_global ref in
      make_judge c (Retyping.get_type_of env Evd.empty c)

  let pretype_sort = function
    | RProp c -> judge_of_prop_contents c
    | RType _ -> judge_of_new_Type ()

  let split_tycon_lam loc env evd tycon =
    let rec real_split evd c =
      let t = whd_betadeltaiota env evd c in
	match kind_of_term t with
	| Prod (na,dom,rng) -> evd, (na, dom, rng)
	| Evar ev when not (Evd.is_defined_evar evd ev) ->
	    let (evd',prod) = define_evar_as_product evd ev in
	    let (_,dom,rng) = destProd prod in
	      evd',(Anonymous, dom, rng)
	| _ -> error_not_product_loc loc env evd c
    in
      match tycon with
      | None -> evd,(Anonymous,None,None)
      | Some (abs, c) ->
	  (match abs with
	   | None ->
	       let evd', (n, dom, rng) = real_split evd c in
		 evd', (n, mk_tycon dom, mk_tycon rng)
	   | Some (init, cur) ->
	       evd, (Anonymous, None, Some (Some (init, succ cur), c)))
	    
	    
  (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
  (* in environment [env], with existential variables [( evdref)] and *)
  (* the type constraint tycon *)
  let rec pretype (tycon : type_constraint) env evdref lvar c =
(*     let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *)
(* 			       str " with tycon " ++ Evarutil.pr_tycon env tycon)  *)
(*     with _ -> () *)
(*     in *)
    match c with
    | RRef (loc,ref) ->
	inh_conv_coerce_to_tycon loc env evdref
	  (pretype_ref evdref env ref)
	  tycon

    | RVar (loc, id) ->
	inh_conv_coerce_to_tycon loc env evdref
	  (pretype_id loc env !evdref lvar id)
	  tycon

    | REvar (loc, ev, instopt) ->
	(* Ne faudrait-il pas s'assurer que hyps est bien un
	   sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
	let hyps = evar_context (Evd.find ( !evdref) ev) in
	let args = match instopt with
          | None -> instance_from_named_context hyps
          | Some inst -> failwith "Evar subtitutions not implemented" in
	let c = mkEvar (ev, args) in
	let j = (Retyping.get_judgment_of env ( !evdref) c) in
	  inh_conv_coerce_to_tycon loc env evdref j tycon

    | RPatVar (loc,(someta,n)) ->
	anomaly "Found a pattern variable in a rawterm to type"

    | RHole (loc,k) ->
	let ty =
          match tycon with
            | Some (None, ty) -> ty
            | None | Some _ ->
		e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
	  { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }

    | RRec (loc,fixkind,names,bl,lar,vdef) ->
	let rec type_bl env ctxt = function
            [] -> ctxt
          | (na,k,None,ty)::bl ->
              let ty' = pretype_type empty_valcon env evdref lvar ty in
              let dcl = (na,None,ty'.utj_val) in
		type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
          | (na,k,Some bd,ty)::bl ->
              let ty' = pretype_type empty_valcon env evdref lvar ty in
              let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar ty in
              let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
		type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
	let ctxtv = Array.map (type_bl env empty_rel_context) bl in
	let larj =
          array_map2
            (fun e ar ->
               pretype_type empty_valcon (push_rel_context e env) evdref lvar ar)
            ctxtv lar in
	let lara = Array.map (fun a -> a.utj_val) larj in
	let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
	let nbfix = Array.length lar in
	let names = Array.map (fun id -> Name id) names in
	  (* Note: bodies are not used by push_rec_types, so [||] is safe *)
	let newenv =
	  let marked_ftys =
	    Array.map (fun ty -> let sort = Retyping.get_type_of env !evdref ty in
			 mkApp (delayed_force Subtac_utils.fix_proto, [| sort; ty |]))
	      ftys
	  in
	    push_rec_types (names,marked_ftys,[||]) env
	in
	let fixi = match fixkind with RFix (vn, i) -> i | RCoFix i -> i in
	let vdefj =
	  array_map2_i
	    (fun i ctxt def ->
	      let fty =
		let ty = ftys.(i) in
		  if i = fixi then (
		    Option.iter (fun tycon ->
		      evdref := Coercion.inh_conv_coerces_to loc env !evdref ftys.(i) tycon)
		      tycon;
		    nf_evar !evdref ty)
		  else ty
	      in
              (* we lift nbfix times the type in tycon, because of
	       * the nbfix variables pushed to newenv *)
              let (ctxt,ty) =
		decompose_prod_n_assum (rel_context_length ctxt)
                  (lift nbfix fty) in
              let nenv = push_rel_context ctxt newenv in
              let j = pretype (mk_tycon ty) nenv evdref lvar def in
		{ uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
		  uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
            ctxtv vdef in
	evar_type_fixpoint loc env evdref names ftys vdefj;
	let ftys = Array.map (nf_evar ( !evdref)) ftys in
	let fdefs = Array.map (fun x -> nf_evar ( !evdref) (j_val x)) vdefj in
	let fixj = match fixkind with
	  | RFix (vn,i) ->
	      (* First, let's find the guard indexes. *)
	      (* If recursive argument was not given by user, we try all args.
	         An earlier approach was to look only for inductive arguments,
		 but doing it properly involves delta-reduction, and it finally
                 doesn't seem worth the effort (except for huge mutual
		 fixpoints ?) *)
	      let possible_indexes = Array.to_list (Array.mapi
		(fun i (n,_) -> match n with
		   | Some n -> [n]
		   | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
		vn)
	      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,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 evdref fixj tycon

    | RSort (loc,s) ->
	inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon

    | RApp (loc,f,args) ->
	let length = List.length args in
	let ftycon =
	  let ty =
	    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
	    match ty with
	    | Some (_, t) when Subtac_coercion.disc_subset t = None -> ty
	    | _ -> None
	in
	let fj = pretype ftycon env evdref lvar f in
 	let floc = loc_of_rawconstr f in
	let rec apply_rec env n resj tycon = function
	  | [] -> resj
	  | c::rest ->
	      let argloc = loc_of_rawconstr c in
	      let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
              let resty = whd_betadeltaiota env ( !evdref) resj.uj_type in
      		match kind_of_term resty with
		  | Prod (na,c1,c2) ->
		      Option.iter (fun ty -> evdref :=
			Coercion.inh_conv_coerces_to loc env !evdref resty ty) tycon;
		      let evd, (_, _, tycon) = split_tycon loc env !evdref tycon in
		      evdref := evd;
		      let hj = pretype (mk_tycon (nf_evar !evdref c1)) env evdref lvar c in
		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
		      let typ' = nf_evar !evdref typ in
			apply_rec env (n+1)
			  { uj_val = nf_evar !evdref value;
			    uj_type = nf_evar !evdref typ' }
			  (Option.map (fun (abs, c) -> abs, nf_evar !evdref c) tycon) rest

		  | _ ->
		      let hj = pretype empty_tycon env evdref lvar c in
			error_cant_apply_not_functional_loc
			  (join_loc floc argloc) env ( !evdref)
	      		  resj [hj]
	in
	let resj = j_nf_evar ( !evdref) (apply_rec env 1 fj ftycon args) in
	let resj =
	  match kind_of_term resj.uj_val with
	  | App (f,args) when isInd f or isConst f ->
	      let sigma =  !evdref in
	      let c = mkApp (f,Array.map (whd_evar sigma) args) in
	      let t = Retyping.get_type_of env sigma c in
	      make_judge c t
	  | _ -> resj in
	  inh_conv_coerce_to_tycon loc env evdref resj tycon

    | RLambda(loc,name,k,c1,c2)      ->
	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')
	  evdref tycon
	in
	let (name',dom,rng) = evd_comb1 (split_tycon_lam loc env) evdref tycon' in
	let dom_valcon = valcon_of_tycon dom in
	let j = pretype_type dom_valcon env evdref lvar c1 in
	let var = (name,None,j.utj_val) in
	let j' = pretype rng (push_rel var env) evdref lvar c2 in
	let resj = judge_of_abstraction env name j j' in
	  inh_conv_coerce_to_tycon loc env evdref resj tycon

    | RProd(loc,name,k,c1,c2)        ->
	let j = pretype_type empty_valcon env evdref lvar c1 in
	let var = (name,j.utj_val) in
	let env' = push_rel_assum var env in
	let j' = pretype_type empty_valcon env' evdref lvar c2 in
	let resj =
	  try judge_of_product env name j j'
	  with TypeError _ as e -> Stdpp.raise_with_loc loc e in
	  inh_conv_coerce_to_tycon loc env evdref resj tycon

    | RLetIn(loc,name,c1,c2)      ->
	let j = pretype empty_tycon env evdref lvar c1 in
	let t = refresh_universes j.uj_type in
	let var = (name,Some j.uj_val,t) in
        let tycon = lift_tycon 1 tycon in
	let j' = pretype tycon (push_rel var env) evdref lvar c2 in
	  { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
	    uj_type = subst1 j.uj_val j'.uj_type }

    | RLetTuple (loc,nal,(na,po),c,d) ->
	let cj = pretype empty_tycon env evdref lvar c in
	let (IndType (indf,realargs)) =
	  try find_rectype env ( !evdref) cj.uj_type
	  with Not_found ->
	    let cloc = loc_of_rawconstr c in
	      error_case_not_inductive_loc cloc env ( !evdref) cj
	in
	let cstrs = get_constructors env indf in
	if Array.length cstrs <> 1 then
          user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor");
	let cs = cstrs.(0) in
	  if List.length nal <> cs.cs_nargs then
            user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables");
	let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
          (List.rev nal) cs.cs_args in
	let env_f = push_rels fsign env in
	  (* Make dependencies from arity signature impossible *)
	let arsgn =
	  let arsgn,_ = get_arity env indf in
	    if not !allow_anonymous_refs then
	      List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
	    else arsgn
	in
	    let psign = (na,None,build_dependent_inductive env indf)::arsgn in
	    let nar = List.length arsgn in
	      (match po with
		 | Some p ->
		     let env_p = push_rels psign env in
		     let pj = pretype_type empty_valcon env_p evdref lvar p in
		     let ccl = nf_evar ( !evdref) pj.utj_val in
		     let psign = make_arity_signature env true indf in (* with names *)
		     let p = it_mkLambda_or_LetIn ccl psign in
		     let inst =
		       (Array.to_list cs.cs_concl_realargs)
		       @[build_dependent_constructor cs] in
		     let lp = lift cs.cs_nargs p in
		     let fty = hnf_lam_applist env ( !evdref) lp inst in
		     let fj = pretype (mk_tycon fty) env_f evdref lvar d in
		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
		     let v =
		       let mis,_ = dest_ind_family indf in
		       let ci = make_case_info env mis LetStyle in
			 mkCase (ci, p, cj.uj_val,[|f|]) in
		       { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }

		 | None ->
		     let tycon = lift_tycon cs.cs_nargs tycon in
		     let fj = pretype tycon env_f evdref lvar d in
		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
		     let ccl = nf_evar ( !evdref) fj.uj_type in
		     let ccl =
		       if noccur_between 1 cs.cs_nargs ccl then
			 lift (- cs.cs_nargs) ccl
		       else
			 error_cant_find_case_type_loc loc env ( !evdref)
			   cj.uj_val in
		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
		     let v =
		       let mis,_ = dest_ind_family indf in
		       let ci = make_case_info env mis LetStyle in
			 mkCase (ci, p, cj.uj_val,[|f|] )
		     in
		       { uj_val = v; uj_type = ccl })

    | RIf (loc,c,(na,po),b1,b2) ->
	let cj = pretype empty_tycon env evdref lvar c in
	let (IndType (indf,realargs)) =
	  try find_rectype env ( !evdref) cj.uj_type
	  with Not_found ->
	    let cloc = loc_of_rawconstr c in
	      error_case_not_inductive_loc cloc env ( !evdref) cj in
	let cstrs = get_constructors env indf in
	  if Array.length cstrs <> 2 then
            user_err_loc (loc,"",
			  str "If is only for inductive types with two constructors.");

	  let arsgn =
	    let arsgn,_ = get_arity env indf in
	      if not !allow_anonymous_refs then
		(* Make dependencies from arity signature impossible *)
		List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
	      else arsgn
	  in
	  let nar = List.length arsgn in
	  let psign = (na,None,build_dependent_inductive env indf)::arsgn in
	  let pred,p = match po with
	    | Some p ->
		let env_p = push_rels psign env in
		let pj = pretype_type empty_valcon env_p evdref lvar p in
		let ccl = nf_evar ( !evdref) pj.utj_val in
		let pred = it_mkLambda_or_LetIn ccl psign in
		let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
		let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred;
								     uj_type = typ} tycon
		in
		  jtyp.uj_val, jtyp.uj_type
	    | None ->
		let p = match tycon with
		  | Some (None, ty) -> ty
		  | None | Some _ ->
                      e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ())
		in
		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
	  let pred = nf_evar ( !evdref) pred in
	  let p = nf_evar ( !evdref) p in
	 (*   msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
	  let f cs b =
	    let n = rel_context_length cs.cs_args in
	    let pi = lift n pred in (* liftn n 2 pred ? *)
	    let pi = beta_applist (pi, [build_dependent_constructor cs]) in
	    let csgn =
	      if not !allow_anonymous_refs then
		List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args
	      else
		List.map
		  (fun (n, b, t) ->
		     match n with
                         Name _ -> (n, b, t)
                       | Anonymous -> (Name (id_of_string "H"), b, t))
		cs.cs_args
	    in
	    let env_c = push_rels csgn env in
(* 	      msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
	    let bj = pretype (mk_tycon pi) env_c evdref lvar b in
	      it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
	  let b1 = f cstrs.(0) b1 in
	  let b2 = f cstrs.(1) b2 in
	  let v =
	    let mis,_ = dest_ind_family indf in
	    let ci = make_case_info env mis IfStyle in
	      mkCase (ci, pred, cj.uj_val, [|b1;b2|])
	  in
	    { uj_val = v; uj_type = p }

    | RCases (loc,sty,po,tml,eqns) ->
	Cases.compile_cases loc sty
	  ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
	  tycon env (* loc *) (po,tml,eqns)

    | RCast (loc,c,k) ->
	let cj =
	  match k with
	      CastCoerce ->
		let cj = pretype empty_tycon env evdref lvar c in
		  evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj
	    | CastConv (k,t) ->
		let tj = pretype_type empty_valcon env evdref lvar t in
		let cj = pretype (mk_tycon tj.utj_val) env evdref lvar c in
		  (* User Casts are for helping pretyping, experimentally not to be kept*)
		  (* ... except for Correctness *)
		let v = mkCast (cj.uj_val, k, tj.utj_val) in
		  { uj_val = v; uj_type = tj.utj_val }
	in
	  inh_conv_coerce_to_tycon loc env evdref cj tycon

    | RDynamic (loc,d) ->
	if (Dyn.tag d) = "constr" then
	  let c = constr_out d in
	  let j = (Retyping.get_judgment_of env ( !evdref) c) in
	    j
	      (*inh_conv_coerce_to_tycon loc env evdref j tycon*)
	else
	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic."))

  (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
  and pretype_type valcon env evdref lvar = function
    | RHole loc ->
	(match valcon with
	   | Some v ->
               let s =
		 let sigma =  !evdref in
		 let t = Retyping.get_type_of env sigma v in
		   match kind_of_term (whd_betadeltaiota env sigma t) with
                     | Sort s -> s
                     | Evar ev when is_Type (existential_type sigma ev) ->
			 evd_comb1 (define_evar_as_sort) evdref ev
                     | _ -> anomaly "Found a type constraint which is not a type"
               in
		 { utj_val = v;
		   utj_type = s }
	   | None ->
	       let s = new_Type_sort () in
		 { utj_val = e_new_evar evdref env ~src:loc (mkSort s);
		   utj_type = s})
    | c ->
	let j = pretype empty_tycon env evdref lvar c in
	let loc = loc_of_rawconstr c in
	let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
	  match valcon with
	    | None -> tj
	    | Some v ->
		if e_cumul env evdref v tj.utj_val then tj
		else
		  error_unexpected_type_loc
                    (loc_of_rawconstr c) env ( !evdref) tj.utj_val v

  let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
    let c' = match kind with
      | OfType exptyp ->
	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
	  (pretype tycon env evdref lvar c).uj_val
      | IsType ->
	  (pretype_type empty_valcon env evdref lvar c).utj_val in
    evdref := consider_remaining_unif_problems env !evdref;
    if resolve_classes then
      (evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
	  ~split:true ~fail:fail_evar env !evdref;
       evdref := consider_remaining_unif_problems env !evdref);
    let c = if expand_evar then nf_evar !evdref c' else c' in
    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 (create_evar_defs sigma) in
    let j = pretype empty_tycon env evdref ([],[]) c in
    let evd = consider_remaining_unif_problems env !evdref in
    let j = j_nf_evar evd j in
    check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
    j

  let understand_judgment_tcc evdref env c =
    let j = pretype empty_tycon env evdref ([],[]) c in
    j_nf_evar !evdref j

  (* Raw calls to the unsafe inference machine: boolean says if we must
     fail on unresolved evars; the unsafe_judgment list allows us to
     extend env with some bindings *)

  let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c =
    let evdref = ref (Evd.create_evar_defs sigma) in
    let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in
    !evdref, c

  (** Entry points of the high-level type synthesis algorithm *)

  let understand_gen kind sigma env c =
    snd (ise_pretype_gen true true true sigma env ([],[]) kind c)

  let understand sigma env ?expected_type:exptyp c =
    snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c)

  let understand_type sigma env c =
    snd (ise_pretype_gen true false true sigma env ([],[]) IsType c)

  let understand_ltac expand_evar sigma env lvar kind c =
    ise_pretype_gen expand_evar false true sigma env lvar kind c

  let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
    ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c

  let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c =
    pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c
end

module Default : S = SubtacPretyping_F(Coercion.Default)