From e193bc26b8dcd2c24b68054f6d4ab8e5986d357c Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 14 Mar 2012 13:33:12 +0000
Subject: Fix merge and add missing file.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15040 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretyping.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 08eaa88673..a9581e8bab 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -138,7 +138,6 @@ let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) =
   (* Side-effect *)
   !evdref,c
 
-<<<<<<< HEAD
 (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
 let allow_anonymous_refs = ref false
 
-- 
cgit v1.2.3