diff options
| author | Matthieu Sozeau | 2014-06-24 17:27:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-24 18:53:52 +0200 |
| commit | ff2da62916d9a6bec4aae1a576ce5d396ea9893e (patch) | |
| tree | cc545ccac688a4283f08989563387d763f22b4de | |
| parent | 9f1f8e29baa6d8f8d458740737d0fbd02de31c6c (diff) | |
Fix program cases and inversion tactic to correctly record universe constraints.
Fixes FingerTree contrib.
| -rw-r--r-- | pretyping/cases.ml | 1 | ||||
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/inv.ml | 3 |
3 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b5aeeae3ab..50396d8547 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2155,6 +2155,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in + let _btype = evd_comb1 (Typing.e_type_of env) evdref bbody in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in let branch = diff --git a/tactics/equality.ml b/tactics/equality.ml index 81f133ddc3..63bb846139 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -987,7 +987,7 @@ let find_sigma_data env s = build_sigma_type () let make_tuple env sigma (rterm,rty) lind = assert (dependent (mkRel lind) rty); let sigdata = find_sigma_data env (get_sort_of env sigma rty) in - let a = type_of env sigma (mkRel lind) in + let sigma, a = e_type_of ~refresh:true env sigma (mkRel lind) in let (na,_,_) = lookup_rel lind env in (* We move [lind] to [1] and lift other rels > [lind] by 1 *) let rty = lift (1-lind) (liftn lind (lind+1) rty) in @@ -1089,7 +1089,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let w_type = type_of env sigma w in if Evarconv.e_cumul env evdref w_type a then let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in - applist(exist_term,[w_type;p_i_minus_1;w;tuple_tail]) + applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) else error "Cannot solve a unification problem." | None -> anomaly (Pp.str "Not enough components to build the dependent tuple") diff --git a/tactics/inv.ml b/tactics/inv.ml index dc88795216..ee875ce27d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -74,7 +74,7 @@ let make_inv_predicate env evd indf realargs id status concl = | NoDep -> (* We push the arity and leave concl unchanged *) let hyps_arity,_ = get_arity env indf in - (hyps_arity,concl) + (hyps_arity,concl) | Dep dflt_concl -> if not (occur_var env id concl) then errorlabstrm "make_inv_predicate" @@ -129,6 +129,7 @@ let make_inv_predicate env evd indf realargs id status concl = in let (newconcl, args) = build_concl [] [] 0 realargs in let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in + let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd predicate in (* OK - this predicate should now be usable by res_elimination_then to do elimination on the conclusion. *) predicate, args |