aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
blob: a56280ba832942d0e9fcf174ecbc830534485503 (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
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

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 Classops
open List
open Recordops 
open Evarutil
open Pretype_errors
open Rawterm
open Evarconv
open Coercion
open Pattern
open Dyn


let evd_comb0 f isevars =
  let (evd',x) = f !isevars in
  isevars := evd';
  x
let evd_comb1 f isevars x =
  let (evd',y) = f !isevars x in
  isevars := evd';
  y
let evd_comb2 f isevars x y =
  let (evd',z) = f !isevars x y in
  isevars := evd';
  z
let evd_comb3 f isevars x y z =
  let (evd',t) = f !isevars x y z in
  isevars := evd';
  t

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

let lift_context n l = 
  let k = List.length l in 
  list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l

(* Tells if a given predicate in v7 syntax is dependent or not *)

let is_dep_arity env kelim predty nodep_ar = 
  let rec srec pt nodep_ar =
    let pt' = whd_betadeltaiota env Evd.empty pt in
    match kind_of_term pt', kind_of_term nodep_ar with
      | Prod (_,a1,a2), Prod (_,a1',a2') -> srec a2 a2'
      | Prod (_,a1,a2), _ -> true
      | _ -> false in 
  srec predty nodep_ar

let is_dependent_elimination env predty indf =
  let (ind,params) = dest_ind_family indf in
  let (_,mip) = Inductive.lookup_mind_specif env ind in
  let kelim = mip.mind_kelim in
  let arsign,s = get_arity env indf in
  let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in
  is_dep_arity env kelim predty glob_t

(* Interpret v7 Match construct *)

let transform_rec loc env sigma (pj,c,lf) indt = 
  let p = pj.uj_val in
  let (indf,realargs) = dest_ind_type indt in
  let (ind,params) = dest_ind_family indf in
  let (mib,mip) = lookup_mind_specif env ind in
  let recargs = mip.mind_recargs in
  let mI = mkInd ind in
  let ci = make_default_case_info env (if Options.do_translate() then RegularStyle else MatchStyle) ind in
  let nconstr = Array.length mip.mind_consnames in
  if Array.length lf <> nconstr then 
    (let cj = {uj_val=c; uj_type=mkAppliedInd indt} in
     error_number_branches_loc loc env sigma cj nconstr);
  let tyi = snd ind in
  if mis_is_recursive_subset [tyi] recargs then
    let dep =
      is_dependent_elimination env (nf_evar sigma pj.uj_type) indf in 
    let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in
    let depFvec = Array.init mib.mind_ntypes init_depFvec in
    (* build now the fixpoint *)
    let lnames,_ = get_arity env indf in
    let nar = List.length lnames in
    let nparams = mip.mind_nparams in
    let constrs = get_constructors env (lift_inductive_family (nar+2) indf) in
    let branches = 
      array_map3
	(fun f t reca -> 
	   whd_beta
             (Indrec.make_rec_branch_arg env sigma
                (nparams,depFvec,nar+1)
                f t reca))
        (Array.map (lift (nar+2)) lf) constrs (dest_subterms recargs) 
    in 
    let deffix = 
      it_mkLambda_or_LetIn_name env
	(lambda_create env
	   (applist (mI,List.append (List.map (lift (nar+1)) params)
                       (extended_rel_list 0 lnames)),
            mkCase (ci, lift (nar+2) p, mkRel 1, branches)))
        (lift_rel_context 1 lnames) 
    in
    if noccurn 1 deffix then 
      whd_beta (applist (pop deffix,realargs@[c]))
    else
      let ind = applist (mI,(List.append 
			     (List.map (lift nar) params)
			     (extended_rel_list 0 lnames))) in
      let typPfix = 
	it_mkProd_or_LetIn_name env
	  (prod_create env 
	     (ind,
	      (if dep then
		 let ext_lnames = (Anonymous,None,ind)::lnames in
		 let args = extended_rel_list 0 ext_lnames in
		 whd_beta (applist (lift (nar+1) p, args))
	       else
		 let args = extended_rel_list 1 lnames in
		 whd_beta (applist (lift (nar+1) p, args)))))
          lnames in
      let fix =
        mkFix (([|nar|],0),
	       ([|Name(id_of_string "F")|],[|typPfix|],[|deffix|])) in
      applist (fix,realargs@[c])
  else
    mkCase (ci, p, c, lf)

(************************************************************************)

(* To embed constr in rawconstr *)
let ((constr_in : constr -> Dyn.t),
     (constr_out : Dyn.t -> constr)) = create "constr"

let mt_evd = Evd.empty

let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)

(* 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 isevars 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 isevars (vdefj.(i)).uj_type
		  (lift lt lar.(i))) then
          error_ill_typed_rec_body_loc loc env (evars_of !isevars)
            i lna vdefj lar
      done

let check_branches_message loc env isevars c (explft,lft) = 
  for i = 0 to Array.length explft - 1 do
    if not (e_cumul env isevars lft.(i) explft.(i)) then 
      let sigma = evars_of !isevars 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 isevars j = function
   | None -> j
   | Some typ -> evd_comb2 (inh_conv_coerce_to loc env) isevars j typ

let push_rels vars env = List.fold_right push_rel vars env

(*
let evar_type_case isevars env ct pt lft p c =
  let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c
  in check_branches_message isevars 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 pretype_id loc env (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 = type_app (lift n) typ }
  with Not_found ->
  try
    List.assoc id lvar
  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 (string_of_id id ^ " ist not 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=lam_it ccl' sign; uj_type=prod_it s' sign} 

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

let pretype_ref isevars 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 ()

(* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
(* in environment [env], with existential variables [(evars_of isevars)] and *)
(* the type constraint tycon *)
let rec pretype tycon env isevars lvar = function

  | RRef (loc,ref) ->
      inh_conv_coerce_to_tycon loc env isevars
	(pretype_ref isevars env ref)
	tycon

  | RVar (loc, id) ->
      inh_conv_coerce_to_tycon loc env isevars
	(pretype_id loc env 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 = (Evd.map (evars_of !isevars) ev).evar_hyps 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 (evars_of !isevars) c) in
      inh_conv_coerce_to_tycon loc env isevars 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 ty -> ty
          | None ->
              e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
      { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }

  | RRec (loc,fixkind,names,bl,lar,vdef) ->
      let rec type_bl env ctxt = function
          [] -> ctxt
        | (na,None,ty)::bl ->
            let ty' = pretype_type empty_valcon env isevars lvar ty in
            let dcl = (na,None,ty'.utj_val) in
            type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
        | (na,Some bd,ty)::bl ->
            let ty' = pretype_type empty_valcon env isevars lvar ty in
            let bd' = pretype (mk_tycon ty'.utj_val) env isevars 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) isevars 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 = push_rec_types (names,ftys,[||]) env in
      let vdefj =
	array_map2_i 
	  (fun i ctxt def ->
            (* 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 ftys.(i)) in
            let nenv = push_rel_context ctxt newenv in
            let j = pretype (mk_tycon ty) nenv isevars 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 isevars names ftys vdefj;
      let fixj =
	match fixkind with
	  | RFix (vn,i as vni) ->
	      let fix = (vni,(names,ftys,Array.map j_val vdefj)) in
	      (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
	      make_judge (mkFix fix) ftys.(i)
	  | RCoFix i -> 
	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) 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 isevars fixj tycon

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

  | RApp (loc,f,args) -> 
      let fj = pretype empty_tycon env isevars lvar f in
      let floc = loc_of_rawconstr f in
      let rec apply_rec env n resj = function
	| [] -> resj
	| c::rest ->
	    let argloc = loc_of_rawconstr c in
	    let resj = evd_comb1 (inh_app_fun env) isevars resj in
            let resty =
              whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
      	    match kind_of_term resty with
	      | Prod (na,c1,c2) ->
		  let hj = pretype (mk_tycon c1) env isevars lvar c in
		  let newresj =
      		    { uj_val = applist (j_val resj, [j_val hj]);
		      uj_type = subst1_nf_evar (evars_of !isevars)
		                hj.uj_val c2 } in
		  apply_rec env (n+1) newresj rest

	      | _ ->
		  let hj = pretype empty_tycon env isevars lvar c in
		  error_cant_apply_not_functional_loc 
		    (join_loc floc argloc) env (evars_of !isevars)
	      	    resj [hj]

      in let resj = apply_rec env 1 fj args in
      (*
	let apply_one_arg (floc,tycon,jl) c =
	let (dom,rng) = split_tycon floc env isevars tycon in
	let cj = pretype dom env isevars lvar c in
	let rng_tycon =
	  option_app (subst1_nf_evar (evars_of !isevars) cj.uj_val) rng in
	let argloc = loc_of_rawconstr c in
	(join_loc floc argloc,rng_tycon,(argloc,cj)::jl)  in
	let _,_,jl =
	List.fold_left apply_one_arg (floc,mk_tycon j.uj_type,[]) args in
	let jl = List.rev jl in
	let resj = inh_apply_rel_list loc env isevars jl (floc,j) tycon in
      *)
      inh_conv_coerce_to_tycon loc env isevars resj tycon

  | RLambda(loc,name,c1,c2)      ->
      let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
      let dom_valcon = valcon_of_tycon dom in
      let j = pretype_type dom_valcon env isevars lvar c1 in
      let var = (name,None,j.utj_val) in
      let j' = pretype rng (push_rel var env) isevars lvar c2 in 
      judge_of_abstraction env name j j'

  | RProd(loc,name,c1,c2)        ->
      let j = pretype_type empty_valcon env isevars 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' isevars 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 isevars resj tycon
	
  | RLetIn(loc,name,c1,c2)      ->
      let j = pretype empty_tycon env isevars lvar c1 in
      let t = refresh_universes j.uj_type in
      let var = (name,Some j.uj_val,t) in
        let tycon = option_app (lift 1) tycon in
      let j' = pretype tycon (push_rel var env) isevars lvar c2 in
      { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
	uj_type = subst1_nf_evar (evars_of !isevars) j.uj_val j'.uj_type }

  | RLetTuple (loc,nal,(na,po),c,d) ->
      let cj = pretype empty_tycon env isevars lvar c in
      let (IndType (indf,realargs) as indt) = 
	try find_rectype env (evars_of !isevars) cj.uj_type
	with Not_found ->
	  let cloc = loc_of_rawconstr c in
	  error_case_not_inductive_loc cloc env (evars_of !isevars) 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,_ = get_arity env indf in
      let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) 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 isevars lvar p in
             let ccl = nf_evar (evars_of !isevars) 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 (evars_of !isevars) lp inst in
	     let fj = pretype (mk_tycon fty) env_f isevars 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_default_case_info env LetStyle mis in
	       mkCase (ci, p, cj.uj_val,[|f|]) in 
             let cs = build_dependent_constructor cs in
	     { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }

	 | None -> 
             let tycon = option_app (lift cs.cs_nargs) tycon in
	     let fj = pretype tycon env_f isevars lvar d in
	     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
	     let ccl = nf_evar (evars_of !isevars) 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 (evars_of !isevars) 
                   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_default_case_info env LetStyle mis in
	       mkCase (ci, p, cj.uj_val,[|f|] ) 
	     in
	     { uj_val = v; uj_type = ccl })

  (* Special Case for let constructions to avoid exponential behavior *)      
  | ROrderedCase (loc,st,po,c,[|f|],xx) when st <> MatchStyle ->
      let cj = pretype empty_tycon env isevars lvar c in
      let (IndType (indf,realargs) as indt) = 
	try find_rectype env (evars_of !isevars) cj.uj_type
	with Not_found ->
	  let cloc = loc_of_rawconstr c in
	  error_case_not_inductive_loc cloc env (evars_of !isevars) cj 
      in
      let j = match po with
	 | Some p ->
             let pj = pretype empty_tycon env isevars lvar p in
             let dep = is_dependent_elimination env pj.uj_type indf in
             let ar =
               arity_of_case_predicate env indf dep (Type (new_univ())) in
             let _ = e_cumul env isevars pj.uj_type ar in
	     let pj = j_nf_evar (evars_of !isevars) pj in
	     let pj = if dep then pj else make_dep_of_undep env indt pj in
	     let (bty,rsty) = 
	       Indrec.type_rec_branches 
		 false env (evars_of !isevars) indt pj.uj_val cj.uj_val 
	     in
	     if Array.length bty <> 1 then
	       error_number_branches_loc 
		 loc env (evars_of !isevars) cj (Array.length bty);
	     let fj = 
	       let tyc = bty.(0) in 
	       pretype (mk_tycon tyc) env isevars lvar f 
	     in
	     let fv = j_val fj in
	     let ft = fj.uj_type in
	     check_branches_message loc env isevars cj.uj_val (bty,[|ft|]);
	     let v =
	       let mis,_ = dest_ind_family indf in
	       let ci = make_default_case_info env st mis in
	       mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val,[|fv|])
	     in 
	     { uj_val = v;  uj_type = rsty }

	 | None -> 
             (* get type information from type of branches *)
	     let expbr = Cases.branch_scheme env isevars false indf in
	     if Array.length expbr <> 1 then
	       error_number_branches_loc loc env (evars_of !isevars) 
		 cj (Array.length expbr);
             let expti = expbr.(0) in
	     let fj = pretype (mk_tycon expti) env isevars lvar f in
	     let use_constraint () =
               (* get type information from constraint *)
               (* warning: if the constraint comes from an evar type, it *)
               (* may be Type while Prop or Set would be expected *)
	       match tycon with
		 | Some pred ->
		     let arsgn = make_arity_signature env true indf in
                     let pred = lift (List.length arsgn) pred in
  		     let pred = 
                       it_mkLambda_or_LetIn (nf_evar (evars_of !isevars) pred)
			 arsgn in
                     false, pred
	         | None ->
                     let sigma = evars_of !isevars in
                     error_cant_find_case_type_loc loc env sigma cj.uj_val
	     in
             let ok, p =
	       try
		 let pred = 
		   Cases.pred_case_ml 
		     env (evars_of !isevars) false indt (0,fj.uj_type) 
		 in 
		 if has_undefined_evars !isevars pred then
		   use_constraint ()
		 else
		   true, pred
	       with Cases.NotInferable _ ->
		 use_constraint ()
	     in 
	     let p = nf_evar (evars_of !isevars) p in
	     let (bty,rsty) =
	       Indrec.type_rec_branches
		 false env (evars_of !isevars) indt p cj.uj_val 
	     in
	     let _ = option_app (e_cumul env isevars rsty) tycon in
	     let fj = 
	       if ok then fj 
	       else pretype (mk_tycon bty.(0)) env isevars lvar f 
	     in
	     let fv = fj.uj_val in
	     let ft = fj.uj_type in
	     let v =
	       let mis,_ = dest_ind_family indf in
	       let ci = make_default_case_info env st mis in
	       mkCase (ci, (nf_betaiota p), cj.uj_val,[|fv|] ) 
	     in
	     { uj_val = v; uj_type = rsty } in

      (* Build the LetTuple form for v8 *)
      let c =
        let (ind,params) = dest_ind_family indf in
        let rtntypopt, indnalopt = match po with
          | None -> None, (Anonymous,None)
          | Some p ->
              let pj = pretype empty_tycon env isevars lvar p in
              let dep = is_dependent_elimination env pj.uj_type indf in
              let rec decomp_lam_force n avoid l p =
                (* avoid is not exhaustive ! *)
                if n = 0 then (List.rev l,p,avoid) else
                  match p with
                    | RLambda (_,(Name id as na),_,c) -> 
                        decomp_lam_force (n-1) (id::avoid) (na::l) c
                    | RLambda (_,(Anonymous as na),_,c) ->
                        decomp_lam_force (n-1) avoid (na::l) c
                    | _ ->
                        let x = Nameops.next_ident_away (id_of_string "x") avoid in
                        decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
                          (* eta-expansion *)
                          (RApp (dummy_loc,p, [RVar (dummy_loc,x)])) in
              let (nal,p,avoid) = 
                decomp_lam_force (List.length realargs) [] [] p in
              let na,rtntyp,_ = 
                if dep then decomp_lam_force 1 avoid [] p
                else [Anonymous],p,[] in
              let intyp =
                if List.for_all
                  (function
                    | Anonymous -> true
                    | Name id -> not (occur_rawconstr id rtntyp)) nal
                then (* No dependency in realargs *)
                  None
                else
                  let args = List.map (fun _ -> Anonymous) params @ nal in
                  Some (dummy_loc,ind,args) in
              (Some rtntyp,(List.hd na,intyp)) in
        let cs = (get_constructors env indf).(0) in
        match indnalopt with
          | (na,None) -> (* Represented as a let *)
              let rec decomp_lam_force n avoid l p =
                if n = 0 then (List.rev l,p) else
                  match p with
                    | RLambda (_,(Name id as na),_,c) -> 
                        decomp_lam_force (n-1) (id::avoid) (na::l) c
                    | RLambda (_,(Anonymous as na),_,c) -> 
                        decomp_lam_force (n-1) avoid (na::l) c
                    | _ ->
                        let x = Nameops.next_ident_away (id_of_string "x") avoid in
                        decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
                          (* eta-expansion *)
                          (let a = RVar (dummy_loc,x) in
                          match p with
                            | RApp (loc,p,l) -> RApp (loc,p,l@[a])
                            | _ -> (RApp (dummy_loc,p,[a]))) in
              let (nal,d) = decomp_lam_force cs.cs_nargs [] [] f in
              RLetTuple (loc,nal,(na,rtntypopt),c,d)
          | _ -> (* Represented as a match *)
            let detype_eqn constr construct_nargs branch =
              let name_cons = function 
                | Anonymous -> fun l -> l
                | Name id -> fun l -> id::l in
              let make_pat na avoid b ids =
                PatVar (dummy_loc,na),
                name_cons na avoid,name_cons na ids
              in
              let rec buildrec ids patlist avoid n b =
                if n=0 then
                  (dummy_loc, ids, 
                  [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
                  b)
                else
                  match b with
	            | RLambda (_,x,_,b) -> 
	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
                        buildrec new_ids (pat::patlist) new_avoid (n-1) b
                          
	            | RLetIn (_,x,_,b) -> 
	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
                        buildrec new_ids (pat::patlist) new_avoid (n-1) b
                          
	            | RCast (_,c,_) ->    (* Oui, il y a parfois des cast *)
	                buildrec ids patlist avoid n c
                        
	            | _ -> (* eta-expansion *)
                        (* nommage de la nouvelle variable *)
                        let id = Nameops.next_ident_away (id_of_string "x") avoid in
	                let new_b = RApp (dummy_loc, b, [RVar(dummy_loc,id)])in
                        let pat,new_avoid,new_ids =
	                  make_pat (Name id) avoid new_b ids in
	                buildrec new_ids (pat::patlist) new_avoid (n-1) new_b
	                  
              in 
              buildrec [] [] [] construct_nargs branch in
            let eqn = detype_eqn (ind,1) cs.cs_nargs f in
            RCases (loc,(po,ref rtntypopt),[c,ref indnalopt],[eqn])
      in
      xx := Some c;
      (* End building the v8 syntax *)
      j

  | RIf (loc,c,(na,po),b1,b2) ->
      let cj = pretype empty_tycon env isevars lvar c in
      let (IndType (indf,realargs) as indt) = 
	try find_rectype env (evars_of !isevars) cj.uj_type
	with Not_found ->
	  let cloc = loc_of_rawconstr c in
	  error_case_not_inductive_loc cloc env (evars_of !isevars) 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");

      (* Make dependencies from arity signature impossible *)
      let arsgn,_ = get_arity env indf in
      let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) 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 isevars lvar p in
            let ccl = nf_evar (evars_of !isevars) pj.utj_val in
	    let pred = it_mkLambda_or_LetIn ccl psign in
	    pred, lift (- nar) (beta_applist (pred,[cj.uj_val]))
	| None -> 
	    let p = match tycon with
	    | Some ty -> ty
	    | None ->
                e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
	    in
	    it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
      let f cs b =
	let n = rel_context_length cs.cs_args in
	let pi = liftn n 2 pred in
	let pi = beta_applist (pi, [build_dependent_constructor cs]) in
	let csgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args in
	let env_c = push_rels csgn env in 
	let bj = pretype (Some pi) env_c isevars 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 pred = nf_evar (evars_of !isevars) pred in
      let p = nf_evar (evars_of !isevars) p in
      let v =
	let mis,_ = dest_ind_family indf in
	let ci = make_default_case_info env IfStyle mis in
	mkCase (ci, pred, cj.uj_val, [|b1;b2|])
      in
      { uj_val = v; uj_type = p }

  | ROrderedCase (loc,st,po,c,lf,x) ->
      let isrec = (st = MatchStyle) in
      let cj = pretype empty_tycon env isevars lvar c in
      let (IndType (indf,realargs) as indt) = 
	try find_rectype env (evars_of !isevars) cj.uj_type
	with Not_found ->
	  let cloc = loc_of_rawconstr c in
	  error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
      let (dep,pj) = match po with
	| Some p ->
            let pj = pretype empty_tycon env isevars lvar p in
            let dep = is_dependent_elimination env pj.uj_type indf in
            let ar =
              arity_of_case_predicate env indf dep (Type (new_univ())) in
            let _ = e_cumul env isevars pj.uj_type ar in
            (dep, pj)
	| None -> 
            (* get type information from type of branches *)
	    let expbr = Cases.branch_scheme env isevars isrec indf in
	    let rec findtype i =
	      if i >= Array.length lf
	      then
                (* get type information from constraint *)
                (* warning: if the constraint comes from an evar type, it *)
                (* may be Type while Prop or Set would be expected *)
	        match tycon with
		  | Some pred ->
		      let arsgn = make_arity_signature env true indf in
                      let pred = lift (List.length arsgn) pred in
  		      let pred = 
			it_mkLambda_or_LetIn (nf_evar (evars_of !isevars) pred)
			  arsgn in
                      (true, 
                       Retyping.get_judgment_of env (evars_of !isevars) pred)
	          | None ->
                      let sigma = evars_of !isevars in
                      error_cant_find_case_type_loc loc env sigma cj.uj_val
	      else
		try
		  let expti = expbr.(i) in
		  let fj =
		    pretype (mk_tycon expti) env isevars lvar lf.(i) in
		  let pred = 
		    Cases.pred_case_ml (* eta-expanse *)
                      env (evars_of !isevars) isrec indt (i,fj.uj_type) in
		  if has_undefined_evars !isevars pred then findtype (i+1)
		  else 
		    let pty =
                      Retyping.get_type_of env (evars_of !isevars) pred in
		    let pj = { uj_val = pred; uj_type = pty } in
(*
                    let _ = option_app (the_conv_x_leq env isevars pred) tycon
                    in
*)
                    (true,pj)
		with Cases.NotInferable _ -> findtype (i+1) in
	    findtype 0 
      in
      let pj = j_nf_evar (evars_of !isevars) pj in
      let pj = if dep then pj else make_dep_of_undep env indt pj in
      let (bty,rsty) =
	Indrec.type_rec_branches
          isrec env (evars_of !isevars) indt pj.uj_val cj.uj_val in
      let _ = option_app (e_cumul env isevars rsty) tycon in
      if Array.length bty <> Array.length lf then
	error_number_branches_loc loc env (evars_of !isevars) 
	  cj (Array.length bty)
      else
	let lfj =
	  array_map2
            (fun tyc f -> pretype (mk_tycon tyc) env isevars lvar f) bty
            lf in
	let lfv = Array.map j_val lfj in
	let lft = Array.map (fun j -> j.uj_type) lfj in
	check_branches_message loc env isevars cj.uj_val (bty,lft);
	let v =
	  if isrec
	  then 
	    transform_rec loc env (evars_of !isevars)(pj,cj.uj_val,lfv) indt
	  else
	    let mis,_ = dest_ind_family indf in
	    let ci = make_default_case_info env st mis in
	    mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val,
                       Array.map (fun j-> j.uj_val) lfj)
	in
        (* Build the Cases form for v8 *)
        let c =
          let (ind,params) = dest_ind_family indf in
          let (mib,mip) = lookup_mind_specif env ind in
          let recargs = mip.mind_recargs in
          let mI = mkInd ind in
          let nconstr = Array.length mip.mind_consnames in
          let tyi = snd ind in
          if isrec && mis_is_recursive_subset [tyi] recargs then
            Some (Detyping.detype (false,env)
	      (ids_of_context env) (names_of_rel_context env)
              (nf_evar (evars_of !isevars) v))
	  else
	    (* Translate into a "match ... with" *)
            let rtntypopt, indnalopt = match po with
              | None -> None, (Anonymous,None)
              | Some p ->
                  let rec decomp_lam_force n avoid l p =
                    (* avoid is not exhaustive ! *)
                    if n = 0 then (List.rev l,p,avoid) else
                      match p with
                        | RLambda (_,(Name id as na),_,c) -> 
                            decomp_lam_force (n-1) (id::avoid) (na::l) c
                        | RLambda (_,(Anonymous as na),_,c) ->
                            decomp_lam_force (n-1) avoid (na::l) c
                        | _ ->
                            let x = Nameops.next_ident_away (id_of_string "x") avoid in
                            decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
                              (* eta-expansion *)
                              (RApp (dummy_loc,p, [RVar (dummy_loc,x)])) in
                  let (nal,p,avoid) = 
                    decomp_lam_force (List.length realargs) [] [] p in
                  let na,rtntyopt,_ = 
                    if dep then decomp_lam_force 1 avoid [] p
                    else [Anonymous],p,[] in
		  let intyp =
		    if nal=[] then None else
                      let args = List.map (fun _ -> Anonymous) params @ nal in
		      Some (dummy_loc,ind,args) in
                  (Some rtntyopt,(List.hd na,intyp)) in
	    let rawbranches =
	      array_map3 (fun bj b cstr ->
		let rec strip n r = if n=0 then r else
		  match r with
		    | RLambda (_,_,_,t) -> strip (n-1) t
		    | RLetIn (_,_,_,t) -> strip (n-1) t
		    | _ -> assert false in
		let n = rel_context_length cstr.cs_args in
		try
		  let _,ccl = decompose_lam_n_assum n bj.uj_val in
		  if noccur_between 1 n ccl then Some (strip n b) else None
		with _ -> (* Not eta-expanded or not reduced *) None)
		lfj lf (get_constructors env indf) in
	    if st = IfStyle & snd indnalopt = None 
	       & rawbranches.(0) <> None && rawbranches.(1) <> None then
	      (* Translate into a "if ... then ... else" *)
	      (* TODO: translate into a "if" even if po is dependent *)
	      Some (RIf (loc,c,(fst indnalopt,rtntypopt),
	          out_some rawbranches.(0),out_some rawbranches.(1)))
	    else
            let detype_eqn constr construct_nargs branch =
              let name_cons = function 
                | Anonymous -> fun l -> l
                | Name id -> fun l -> id::l in
              let make_pat na avoid b ids =
                PatVar (dummy_loc,na),
                name_cons na avoid,name_cons na ids
              in
              let rec buildrec ids patlist avoid n b =
                if n=0 then
                  (dummy_loc, ids, 
                  [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
                  b)
                else
                  match b with
	            | RLambda (_,x,_,b) -> 
	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
                        buildrec new_ids (pat::patlist) new_avoid (n-1) b
                          
	            | RLetIn (_,x,_,b) -> 
	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
                        buildrec new_ids (pat::patlist) new_avoid (n-1) b
                          
	            | RCast (_,c,_) ->    (* Oui, il y a parfois des cast *)
	                buildrec ids patlist avoid n c
                        
	            | _ -> (* eta-expansion *)
                        (* nommage de la nouvelle variable *)
                        let id = Nameops.next_ident_away (id_of_string "x") avoid in
	                let new_b = RApp (dummy_loc, b, [RVar(dummy_loc,id)])in
                        let pat,new_avoid,new_ids =
	                  make_pat (Name id) avoid new_b ids in
	                buildrec new_ids (pat::patlist) new_avoid (n-1) new_b
	                  
              in 
              buildrec [] [] [] construct_nargs branch in
            let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
            let get_consnarg j = 
              let typi = mis_nf_constructor_type (ind,mib,mip) (j+1) in
              let _,t = decompose_prod_n_assum mip.mind_nparams typi in
              List.rev (fst (decompose_prod_assum t)) in
            let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in
            let consnargsl = Array.map List.length consnargs in
            let constructs = Array.init (Array.length lf) (fun i -> (ind,i+1)) in
            let eqns = array_map3 detype_eqn constructs consnargsl lf in
            Some (RCases (loc,(po,ref rtntypopt),[c,ref indnalopt],Array.to_list eqns)) in
        x := c;
        (* End build the Cases form for v8 *)
	{ uj_val = v;
	  uj_type = rsty }

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

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

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

(* [pretype_type valcon env isevars lvar c] coerces [c] into a type *)
and pretype_type valcon env isevars lvar = function
  | RHole loc ->
      (match valcon with
	 | Some v ->
             let s =
               let sigma = evars_of !isevars 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 v when is_Type (existential_type sigma v) -> 
                     evd_comb1 (define_evar_as_sort) isevars v
                 | _ -> 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 isevars env ~src:loc (mkSort s);
	       utj_type = s})
  | c ->
      let j = pretype empty_tycon env isevars lvar c in
      let tj = evd_comb1 (inh_coerce_to_sort env) isevars j in
      match valcon with
	| None -> tj
	| Some v ->
	    if e_cumul env isevars v tj.utj_val then tj
	    else
	      error_unexpected_type_loc
                (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v


let unsafe_infer tycon isevars env lvar constr =
  let j = pretype tycon env isevars lvar constr in
  j_nf_evar (evars_of !isevars) j

let unsafe_infer_type valcon isevars env lvar constr =
  let tj = pretype_type valcon env isevars lvar constr in
  tj_nf_evar (evars_of !isevars) tj

(* If fail_evar is false, [process_evars] builds a meta_map with the
   unresolved Evar that were not in initial sigma; otherwise it fail
   on the first unresolved Evar not already in the initial sigma. *)
(* [fail_evar] says how to process unresolved evars:
 *   true -> raise an error message
 *   false -> convert them into new Metas (casted with their type)
 *)
(* assumes the defined existentials have been replaced in c (should be
   done in unsafe_infer and unsafe_infer_type) *)
let check_evars fail_evar env initial_sigma isevars c =
  let sigma = evars_of !isevars in
  let rec proc_rec c =
    match kind_of_term c with
      | Evar (ev,args as k) ->
          assert (Evd.in_dom sigma ev);
	  if not (Evd.in_dom initial_sigma ev) then
	    (if fail_evar then
              let (loc,k) = evar_source ev !isevars in
	       error_unsolvable_implicit loc env sigma k)
      | _ -> iter_constr proc_rec c      
  in
  proc_rec 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...
*)

(* constr with holes *)
type open_constr = evar_map * constr

let ise_resolve_casted_gen fail_evar sigma env lvar typ c =
  let isevars = ref (create_evar_defs sigma) in
  let j = unsafe_infer (mk_tycon typ) isevars env lvar c in
  check_evars fail_evar env sigma isevars (mkCast(j.uj_val,j.uj_type));
  (evars_of !isevars, j)

let ise_resolve_casted sigma env typ c =
  ise_resolve_casted_gen true sigma env ([],[]) typ c

(* Raw calls to the unsafe inference machine: boolean says if we must fail
   on unresolved evars, or replace them by Metas; the unsafe_judgment list
   allows us to extend env with some bindings *)
let ise_infer_gen fail_evar sigma env lvar exptyp c =
  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
  let isevars = ref (create_evar_defs sigma) in
  let j = unsafe_infer tycon isevars env lvar c in
  check_evars fail_evar env sigma isevars (mkCast(j.uj_val,j.uj_type));
  (evars_of !isevars, j)

let ise_infer_type_gen fail_evar sigma env lvar c =
  let isevars = ref (create_evar_defs sigma) in
  let tj = unsafe_infer_type empty_valcon isevars env lvar c in
  check_evars fail_evar env sigma isevars tj.utj_val;
  (evars_of !isevars, tj)

type var_map = (identifier * unsafe_judgment) list

let understand_judgment sigma env c =
  snd (ise_infer_gen true sigma env ([],[]) None c)

let understand_type_judgment sigma env c =
  snd (ise_infer_type_gen true sigma env ([],[]) c)

let understand sigma env c =
  let _, c = ise_infer_gen true sigma env ([],[]) None c in
  c.uj_val

let understand_type sigma env c =
  let _,c = ise_infer_type_gen true sigma env ([],[]) c in
  c.utj_val

let understand_gen_ltac sigma env lvar ~expected_type:exptyp c =
  let _, c = ise_infer_gen true sigma env lvar exptyp c in
  c.uj_val

let understand_gen sigma env lvar ~expected_type:exptyp c =
  let _, c = ise_infer_gen true sigma env (lvar,[]) exptyp c in
  c.uj_val

let understand_gen_tcc sigma env lvar exptyp c =
  let metamap, c = ise_infer_gen false sigma env (lvar,[]) exptyp c in
  metamap, c.uj_val

let interp_sort = function
  | RProp c -> Prop c
  | RType _ -> new_Type_sort ()

let interp_elimination_sort = function
  | RProp Null -> InProp
  | RProp Pos  -> InSet
  | RType _ -> InType