From d6ba7f4b8fbd98f2f1c848857022ef5fba80db53 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 16 Sep 2009 08:32:32 +0000 Subject: [PATCH] The left parameters coming from the constructor types have been refined in a longer context. Thus we need to unify them in the longer context (that does not hurt those coming from the inductive types). --- helm/software/components/ng_refiner/nCicRefiner.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 56ec069d2..8dc94e9e4 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -746,7 +746,7 @@ let typeof_obj "and those of its inductive type")))) else metasenv,subst,item1::context - ) (metasenv,subst,[]) sx_context_ty_rev sx_context_te_rev + ) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev with Invalid_argument "List.fold_left2" -> assert false in let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in (match -- 2.39.2